diff options
author | Son HO | 2024-03-11 11:10:01 +0100 |
---|---|---|
committer | GitHub | 2024-03-11 11:10:01 +0100 |
commit | c33a9807cf6aa21b2364449ee756ebf93de19eca (patch) | |
tree | 3a58f5a619502521d0a6ff7fe2edd139e275f8f1 /tests/lean/Demo | |
parent | 14171474f9a4a45874d181cdb6567c7af7dc32cd (diff) | |
parent | 157a2364c02293d14b765ebdaec0d2eeae75a1aa (diff) |
Merge pull request #88 from AeneasVerif/son/clashes
Improve the name generation for code extraction
Diffstat (limited to 'tests/lean/Demo')
-rw-r--r-- | tests/lean/Demo/Demo.lean | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean index 01818585..854b4853 100644 --- a/tests/lean/Demo/Demo.lean +++ b/tests/lean/Demo/Demo.lean @@ -126,23 +126,23 @@ 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]: 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 |