From a745e81c9949f24878f788fffd36667739c59330 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 7 Nov 2023 10:44:58 +0100
Subject: Update the extraction

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

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

diff --git a/tests/lean/Traits/Funs.lean b/tests/lean/Traits/Funs.lean
index 156ef1e0..6a2834ff 100644
--- a/tests/lean/Traits/Funs.lean
+++ b/tests/lean/Traits/Funs.lean
@@ -227,6 +227,15 @@ def order1
   :=
   Result.ret ()
 
+/- Trait implementation: [traits::usize::{9}] -/
+def usize.ParentTrait1Inst : ParentTrait1 Usize := {
+}
+
+/- Trait implementation: [traits::usize::{10}] -/
+def usize.ChildTrait1Inst : ChildTrait1 Usize := {
+  parent_clause_0 := usize.ParentTrait1Inst
+}
+
 /- [traits::map_option]: forward function -/
 def map_option
   (T F : Type) (inst : core.ops.function.Fn F T) (x : Option T) (f0 : F) :
-- 
cgit v1.2.3