From 8d342557a3780be6c103ca778023995c4f035e41 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Wed, 13 Nov 2024 16:28:17 +0100 Subject: [PATCH] Make lambda type with generic arguments. --- engine/backends/fstar/fstar_backend.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 1fb59068a..ea609f69d 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -1479,7 +1479,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