2 files changed, 39 insertions, 0 deletions
diff --git a/tests/lean/Traits/Funs.lean b/tests/lean/Traits/Funs.lean
index 6a2834ff..8d423280 100644
--- a/tests/lean/Traits/Funs.lean
+++ b/tests/lean/Traits/Funs.lean
@@ -247,4 +247,29 @@ def map_option
                  let t ← inst.call f0 x0
                  Result.ret (some t)
 
+/- Trait implementation: [traits::u32::{11}] -/
+def u32.WithTargetInst : WithTarget U32 := {
+  Target := U32
+}
+
+/- Trait implementation: [traits::u32::{12}] -/
+def u32.ParentTrait2Inst : ParentTrait2 U32 := {
+  U := U32
+  U_clause_0 := u32.WithTargetInst
+}
+
+/- [traits::u32::{13}::convert]: forward function -/
+def u32.convert (x : U32) : Result U32 :=
+  Result.ret x
+
+/- Trait implementation: [traits::u32::{13}] -/
+def u32.ChildTrait2Inst : ChildTrait2 U32 := {
+  parent_clause_0 := u32.ParentTrait2Inst
+  convert := u32.convert
+}
+
+/- [traits::incr_u32]: forward function -/
+def incr_u32 (x : U32) : Result U32 :=
+  x + 1#u32
+
 end traits
diff --git a/tests/lean/Traits/Types.lean b/tests/lean/Traits/Types.lean
index 20af9cb1..4c5dd874 100644
--- a/tests/lean/Traits/Types.lean
+++ b/tests/lean/Traits/Types.lean
@@ -127,4 +127,18 @@ 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
 
+/- Trait declaration: [traits::WithTarget] -/
+structure WithTarget (Self : Type) where
+  Target : Type
+
+/- Trait declaration: [traits::ParentTrait2] -/
+structure ParentTrait2 (Self : Type) where
+  U : Type
+  U_clause_0 : WithTarget U
+
+/- Trait declaration: [traits::ChildTrait2] -/
+structure ChildTrait2 (Self : Type) where
+  parent_clause_0 : ParentTrait2 Self
+  convert : parent_clause_0.U → Result parent_clause_0.U_clause_0.Target
+
 end traits