From eb9ff46c69b9a95c453d64eee059916130d59846 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 9 Nov 2023 11:22:39 +0100
Subject: Regenerate some Lean tests

---
 tests/lean/Traits/Funs.lean | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

(limited to 'tests/lean/Traits/Funs.lean')

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
-- 
cgit v1.2.3

