2 files changed, 37 insertions, 94 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;
+}
+
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
index 94ae0bb0..12e7eafa 100644
--- a/tests/lean/Traits.lean
+++ b/tests/lean/Traits.lean
@@ -322,51 +322,8 @@ structure FromResidual (Self T : Type) where
 
 /- Trait declaration: [traits::Try] -/
 structure Try (Self : Type) where
-  parent_clause_0 : FromResidual Self Residual
   Residual : Type
-
-/- Trait declaration: [traits::CFnOnce] -/
-structure CFnOnce (Self Args : Type) where
-  Output : Type
-  call_once : Self → Args → Result Output
-
-/- Trait declaration: [traits::CFnMut] -/
-structure CFnMut (Self Args : Type) where
-  parent_clause_0 : CFnOnce Self Args
-  call_mut : Self → Args → Result parent_clause_0.Output
-  call_mut_back : Self → Args → parent_clause_0.Output → Result Self
-
-/- Trait declaration: [traits::CFn] -/
-structure CFn (Self Args : Type) where
-  parent_clause_0 : CFnMut Self Args
-  call_mut : Self → Args → Result parent_clause_0.parent_clause_0.Output
-
-/- Trait declaration: [core::ops::function::FnOnce] -/
-structure core.ops.function.FnOnce (Self Args : Type) where
-  Output : Type
-  call_once : Self → Args → Result Output
-
-/- Trait declaration: [core::ops::function::FnMut] -/
-structure core.ops.function.FnMut (Self Args : Type) where
-  parent_clause_0 : core.ops.function.FnOnce Self Args
-  call_mut : Self → Args → Result parent_clause_0.Output
-  call_mut_back : Self → Args → parent_clause_0.Output → Result Self
-
-/- Trait declaration: [core::ops::function::Fn] -/
-structure core.ops.function.Fn (Self Args : Type) where
-  parent_clause_0 : core.ops.function.FnMut Self Args
-  call : Self → Args → Result parent_clause_0.parent_clause_0.Output
-
-/- [traits::map_option]: forward function -/
-def map_option
-  (T F : Type) (inst : core.ops.function.Fn F T) (x : Option T) (f0 : F) :
-  Result (Option T)
-  :=
-  match x with
-  | none => Result.ret none
-  | some x0 => do
-                 let t ← inst.call f0 x0
-                 Result.ret (some t)
+  parent_clause_0 : FromResidual Self Residual
 
 /- Trait declaration: [traits::WithTarget] -/
 structure WithTarget (Self : Type) where
@@ -407,4 +364,20 @@ def u32.ChildTrait2Inst : ChildTrait2 U32 := {
 def incr_u32 (x : U32) : Result U32 :=
   x + 1#u32
 
+/- Trait declaration: [traits::CFnOnce] -/
+structure CFnOnce (Self Args : Type) where
+  Output : Type
+  call_once : Self → Args → Result Output
+
+/- Trait declaration: [traits::CFnMut] -/
+structure CFnMut (Self Args : Type) where
+  parent_clause_0 : CFnOnce Self Args
+  call_mut : Self → Args → Result parent_clause_0.Output
+  call_mut_back : Self → Args → parent_clause_0.Output → Result Self
+
+/- Trait declaration: [traits::CFn] -/
+structure CFn (Self Args : Type) where
+  parent_clause_0 : CFnMut Self Args
+  call_mut : Self → Args → Result parent_clause_0.parent_clause_0.Output
+
 end traits