Merge pull request #891 from hacspec/improve-default-trait

fix: fstar: default trait
cryspen · Sep 16, 2024 · cc29a3f · cc29a3f
2 parents 4511585 + 9ac42a2
commit cc29a3f
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/proof-libs/fstar/core/Core.Default.fsti b/proof-libs/fstar/core/Core.Default.fsti
@@ -1,5 +1,7 @@
 module Core.Default
 
 class t_Default (t: Type0) = {
-  v_default: unit -> t;
+  f_default_pre: unit -> Type0;
+  f_default_post: unit -> out:t -> Type0;
+  f_default: unit -> t;
 }