Make lambda type with generic arguments.

cryspen · Nov 13, 2024 · b3f92d6 · b3f92d6
1 parent 8ea94cd
commit b3f92d6
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
@@ -1478,7 +1478,9 @@ struct
         let impl_val = ctx.interface_mode && not has_type in
         let let_impl = F.AST.TopLevelLet (NoLetQualifier, [ (pat, body) ]) in
         if impl_val then
-          let v = F.AST.Val (name, typ) in
+          let generics_types = List.map ~f:FStarBinder.to_typ generics in
+          let val_type = F.mk_e_arrow generics_types typ in
+          let v = F.AST.Val (name, val_type) in
           (F.decls ~fsti:true ~attrs:[ tcinst ] @@ v)
           @ F.decls ~fsti:false ~attrs:[ tcinst ] let_impl
         else F.decls ~fsti:ctx.interface_mode ~attrs:[ tcinst ] let_impl