From bf0b35b9b1fa90d50587e906432077b63a9ad34d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 11 Mar 2024 09:43:21 +0100
Subject: Update the generated files

---
 tests/lean/Demo/Demo.lean | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'tests/lean/Demo/Demo.lean')

diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
index 01818585..b6a4a797 100644
--- a/tests/lean/Demo/Demo.lean
+++ b/tests/lean/Demo/Demo.lean
@@ -126,17 +126,17 @@ divergent def i32_id (i : I32) : Result I32 :=
 structure Counter (Self : Type) where
   incr : Self → Result (Usize × Self)
 
-/- [demo::{usize}::incr]:
+/- [demo::{(demo::Counter for usize)}::incr]:
    Source: 'src/demo.rs', lines 88:4-88:31 -/
-def Usize.incr (self : Usize) : Result (Usize × Usize) :=
+def CounterUsize.incr (self : Usize) : Result (Usize × Usize) :=
   do
   let self1 ← self + 1#usize
   Result.ret (self, self1)
 
-/- Trait implementation: [demo::{usize}]
+/- Trait implementation: [demo::{(demo::Counter for usize)}]
    Source: 'src/demo.rs', lines 87:0-87:22 -/
-def demo.CounterUsizeInst : Counter Usize := {
-  incr := Usize.incr
+def CounterUsize : Counter Usize := {
+  incr := CounterUsize.incr
 }
 
 /- [demo::use_counter]:
-- 
cgit v1.2.3


From 21fdbab049534b35e9573da89bdfd5942144cbb9 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 11 Mar 2024 10:20:15 +0100
Subject: Regenerate the test files

---
 tests/lean/Demo/Demo.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tests/lean/Demo/Demo.lean')

diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
index b6a4a797..854b4853 100644
--- a/tests/lean/Demo/Demo.lean
+++ b/tests/lean/Demo/Demo.lean
@@ -142,7 +142,7 @@ def CounterUsize : Counter Usize := {
 /- [demo::use_counter]:
    Source: 'src/demo.rs', lines 95:0-95:59 -/
 def use_counter
-  (T : Type) (CounterTInst : Counter T) (cnt : T) : Result (Usize × T) :=
-  CounterTInst.incr cnt
+  (T : Type) (CounterInst : Counter T) (cnt : T) : Result (Usize × T) :=
+  CounterInst.incr cnt
 
 end demo
-- 
cgit v1.2.3