summaryrefslogtreecommitdiff
path: root/tests/fstar/traits/Traits.fst
diff options
context:
space:
mode:
authorSon Ho2023-11-09 13:44:03 +0100
committerSon Ho2023-11-09 13:44:03 +0100
commit38a01551719d0cefdd4a1c21a050674154b0b087 (patch)
treea5df3c2174de4787ab006e71a1fefcc87066a1e7 /tests/fstar/traits/Traits.fst
parent2438e99c6d5a368da59dfa77a400246a8bc55d39 (diff)
Regenerate the tests
Diffstat (limited to 'tests/fstar/traits/Traits.fst')
-rw-r--r--tests/fstar/traits/Traits.fst70
1 files changed, 20 insertions, 50 deletions
diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst
index 42b43cf2..318efa2b 100644
--- a/tests/fstar/traits/Traits.fst
+++ b/tests/fstar/traits/Traits.fst
@@ -308,59 +308,10 @@ type fromResidual_t (self t : Type0) = unit
(** Trait declaration: [traits::Try] *)
noeq type try_t (self : Type0) = {
- parent_clause_0 : fromResidual_t self tResidual;
tResidual : Type0;
+ parent_clause_0 : fromResidual_t self tResidual;
}
-(** Trait declaration: [traits::CFnOnce] *)
-noeq type cFnOnce_t (self args : Type0) = {
- tOutput : Type0;
- call_once : self -> args -> result tOutput;
-}
-
-(** Trait declaration: [traits::CFnMut] *)
-noeq type cFnMut_t (self args : Type0) = {
- parent_clause_0 : cFnOnce_t self args;
- call_mut : self -> args -> result parent_clause_0.tOutput;
- call_mut_back : self -> args -> parent_clause_0.tOutput -> result self;
-}
-
-(** Trait declaration: [traits::CFn] *)
-noeq type cFn_t (self args : Type0) = {
- parent_clause_0 : cFnMut_t self args;
- call_mut : self -> args -> result parent_clause_0.parent_clause_0.tOutput;
-}
-
-(** Trait declaration: [core::ops::function::FnOnce] *)
-noeq type core_ops_function_FnOnce_t (self args : Type0) = {
- tOutput : Type0;
- call_once : self -> args -> result tOutput;
-}
-
-(** Trait declaration: [core::ops::function::FnMut] *)
-noeq type core_ops_function_FnMut_t (self args : Type0) = {
- parent_clause_0 : core_ops_function_FnOnce_t self args;
- call_mut : self -> args -> result parent_clause_0.tOutput;
- call_mut_back : self -> args -> parent_clause_0.tOutput -> result self;
-}
-
-(** Trait declaration: [core::ops::function::Fn] *)
-noeq type core_ops_function_Fn_t (self args : Type0) = {
- parent_clause_0 : core_ops_function_FnMut_t self args;
- call : self -> args -> result parent_clause_0.parent_clause_0.tOutput;
-}
-
-(** [traits::map_option]: forward function *)
-let map_option
- (t f0 : Type0) (inst : core_ops_function_Fn_t f0 t) (x : option t)
- (f1 : f0) :
- result (option t)
- =
- begin match x with
- | None -> Return None
- | Some x0 -> let* x1 = inst.call f1 x0 in Return (Some x1)
- end
-
(** Trait declaration: [traits::WithTarget] *)
noeq type withTarget_t (self : Type0) = { tTarget : Type0; }
@@ -399,3 +350,22 @@ let u32_ChildTrait2Inst : childTrait2_t u32 = {
let incr_u32 (x : u32) : result u32 =
u32_add x 1
+(** Trait declaration: [traits::CFnOnce] *)
+noeq type cFnOnce_t (self args : Type0) = {
+ tOutput : Type0;
+ call_once : self -> args -> result tOutput;
+}
+
+(** Trait declaration: [traits::CFnMut] *)
+noeq type cFnMut_t (self args : Type0) = {
+ parent_clause_0 : cFnOnce_t self args;
+ call_mut : self -> args -> result parent_clause_0.tOutput;
+ call_mut_back : self -> args -> parent_clause_0.tOutput -> result self;
+}
+
+(** Trait declaration: [traits::CFn] *)
+noeq type cFn_t (self args : Type0) = {
+ parent_clause_0 : cFnMut_t self args;
+ call_mut : self -> args -> result parent_clause_0.parent_clause_0.tOutput;
+}
+