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') 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