From 184e27bce209f7a852c2adc7e0598ed75ac8452d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 21 Nov 2023 18:58:04 +0100
Subject: Regenerate the files

---
 tests/lean/Traits.lean | 38 +++++++++++++++++++++-----------------
 1 file changed, 21 insertions(+), 17 deletions(-)

(limited to 'tests/lean')

diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
index f854da76..0aa68c5e 100644
--- a/tests/lean/Traits.lean
+++ b/tests/lean/Traits.lean
@@ -170,7 +170,7 @@ def h3
 /- Trait declaration: [traits::OfTypeBis]
    Source: 'src/traits.rs', lines 109:0-109:36 -/
 structure OfTypeBis (Self T : Type) where
-  parent_clause_0 : ToType T Self
+  ToTypeTSelfInst : ToType T Self
   of_type : T → Result Self
 
 /- [traits::h4]: forward function
@@ -327,20 +327,22 @@ structure ParentTrait1 (Self : Type) where
 /- Trait declaration: [traits::ChildTrait]
    Source: 'src/traits.rs', lines 206:0-206:49 -/
 structure ChildTrait (Self : Type) where
-  parent_clause_0 : ParentTrait0 Self
-  parent_clause_1 : ParentTrait1 Self
+  ParentTrait0SelfInst : ParentTrait0 Self
+  ParentTrait1SelfInst : ParentTrait1 Self
 
 /- [traits::test_child_trait1]: forward function
    Source: 'src/traits.rs', lines 209:0-209:56 -/
 def test_child_trait1
   (T : Type) (inst : ChildTrait T) (x : T) : Result alloc.string.String :=
-  inst.parent_clause_0.get_name x
+  inst.ParentTrait0SelfInst.get_name x
 
 /- [traits::test_child_trait2]: forward function
    Source: 'src/traits.rs', lines 213:0-213:54 -/
 def test_child_trait2
-  (T : Type) (inst : ChildTrait T) (x : T) : Result inst.parent_clause_0.W :=
-  inst.parent_clause_0.get_w x
+  (T : Type) (inst : ChildTrait T) (x : T) :
+  Result inst.ParentTrait0SelfInst.W
+  :=
+  inst.ParentTrait0SelfInst.get_w x
 
 /- [traits::order1]: forward function
    Source: 'src/traits.rs', lines 219:0-219:59 -/
@@ -353,7 +355,7 @@ def order1
 /- Trait declaration: [traits::ChildTrait1]
    Source: 'src/traits.rs', lines 222:0-222:35 -/
 structure ChildTrait1 (Self : Type) where
-  parent_clause_0 : ParentTrait1 Self
+  ParentTrait1SelfInst : ParentTrait1 Self
 
 /- Trait implementation: [traits::{usize#9}]
    Source: 'src/traits.rs', lines 224:0-224:27 -/
@@ -363,7 +365,7 @@ def traits.ParentTrait1UsizeInst : ParentTrait1 Usize := {
 /- Trait implementation: [traits::{usize#10}]
    Source: 'src/traits.rs', lines 225:0-225:26 -/
 def traits.ChildTrait1UsizeInst : ChildTrait1 Usize := {
-  parent_clause_0 := traits.ParentTrait1UsizeInst
+  ParentTrait1SelfInst := traits.ParentTrait1UsizeInst
 }
 
 /- Trait declaration: [traits::Iterator]
@@ -387,7 +389,7 @@ structure FromResidual (Self T : Type) where
    Source: 'src/traits.rs', lines 246:0-246:48 -/
 structure Try (Self : Type) where
   Residual : Type
-  parent_clause_0 : FromResidual Self Residual
+  FromResidualSelftraitsTrySelfResidualInst : FromResidual Self Residual
 
 /- Trait declaration: [traits::WithTarget]
    Source: 'src/traits.rs', lines 252:0-252:20 -/
@@ -403,8 +405,9 @@ structure ParentTrait2 (Self : Type) where
 /- Trait declaration: [traits::ChildTrait2]
    Source: 'src/traits.rs', lines 260:0-260:35 -/
 structure ChildTrait2 (Self : Type) where
-  parent_clause_0 : ParentTrait2 Self
-  convert : parent_clause_0.U → Result parent_clause_0.U_clause_0.Target
+  ParentTrait2SelfInst : ParentTrait2 Self
+  convert : ParentTrait2SelfInst.U → Result
+    ParentTrait2SelfInst.U_clause_0.Target
 
 /- Trait implementation: [traits::{u32#11}]
    Source: 'src/traits.rs', lines 264:0-264:23 -/
@@ -427,7 +430,7 @@ def U32.convert (x : U32) : Result U32 :=
 /- Trait implementation: [traits::{u32#13}]
    Source: 'src/traits.rs', lines 272:0-272:24 -/
 def traits.ChildTrait2U32Inst : ChildTrait2 U32 := {
-  parent_clause_0 := traits.ParentTrait2U32Inst
+  ParentTrait2SelfInst := traits.ParentTrait2U32Inst
   convert := U32.convert
 }
 
@@ -440,15 +443,16 @@ structure CFnOnce (Self Args : Type) where
 /- Trait declaration: [traits::CFnMut]
    Source: 'src/traits.rs', lines 292:0-292:37 -/
 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
+  CFnOnceSelfArgsInst : CFnOnce Self Args
+  call_mut : Self → Args → Result CFnOnceSelfArgsInst.Output
+  call_mut_back : Self → Args → CFnOnceSelfArgsInst.Output → Result Self
 
 /- Trait declaration: [traits::CFn]
    Source: 'src/traits.rs', lines 296:0-296:33 -/
 structure CFn (Self Args : Type) where
-  parent_clause_0 : CFnMut Self Args
-  call_mut : Self → Args → Result parent_clause_0.parent_clause_0.Output
+  CFnMutSelfArgsInst : CFnMut Self Args
+  call_mut : Self → Args → Result
+    CFnMutSelfArgsInst.CFnOnceSelfArgsInst.Output
 
 /- [traits::incr_u32]: forward function
    Source: 'src/traits.rs', lines 300:0-300:30 -/
-- 
cgit v1.2.3