Fstar val instances

engine/backends/fstar/fstar_backend.ml

@@ -1338,8 +1338,10 @@ struct
         in
         let body = F.term @@ F.AST.Record (None, fields) in
         let tcinst = F.term @@ F.AST.Var FStar_Parser_Const.tcinstance_lid in
-        F.decls ~fsti:ctx.interface_mode ~attrs:[ tcinst ]
-        @@ F.AST.TopLevelLet (NoLetQualifier, [ (pat, body) ])
+        [
+          F.decl ~fsti:false ~attrs:[ tcinst ] @@ F.AST.TopLevelLet (NoLetQualifier, [ (pat, body) ]);
+          F.decl ~fsti:true ~attrs:[ tcinst ] @@ F.AST.Val (name, typ);
+        ]
     | Quote quote ->
         let fstar_opts =
           Attrs.find_unique_attr e.attrs ~f:(function

engine/lib/dependencies.ml

@@ -59,7 +59,7 @@ module Make (F : Features.T) = struct
             @ v#visit_ty () self_ty
             @ v#visit_global_ident () (fst of_trait)
             @ concat_map (v#visit_generic_value ()) (snd of_trait)
-            @ concat_map (v#visit_impl_item ()) items
+            (* @ concat_map (v#visit_impl_item ()) items *)
             @ concat_map
                 (fun (ie, ii) ->
                   v#visit_impl_expr () ie @ v#visit_impl_ident () ii)

proof-libs/fstar/core/Core.Default.fsti

@@ -0,0 +1,5 @@
+module Core.Default
+
+class t_Default (t: Type0) = {
+  v_default: unit -> t;
+}