diff options
author | Son Ho | 2023-11-09 13:44:03 +0100 |
---|---|---|
committer | Son Ho | 2023-11-09 13:44:03 +0100 |
commit | 38a01551719d0cefdd4a1c21a050674154b0b087 (patch) | |
tree | a5df3c2174de4787ab006e71a1fefcc87066a1e7 /tests/fstar | |
parent | 2438e99c6d5a368da59dfa77a400246a8bc55d39 (diff) |
Regenerate the tests
Diffstat (limited to '')
-rw-r--r-- | tests/fstar/traits/Traits.fst | 70 |
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; +} + |