summaryrefslogtreecommitdiff
path: root/tests/lean/Demo
diff options
context:
space:
mode:
authorSon HO2024-03-11 11:10:01 +0100
committerGitHub2024-03-11 11:10:01 +0100
commitc33a9807cf6aa21b2364449ee756ebf93de19eca (patch)
tree3a58f5a619502521d0a6ff7fe2edd139e275f8f1 /tests/lean/Demo
parent14171474f9a4a45874d181cdb6567c7af7dc32cd (diff)
parent157a2364c02293d14b765ebdaec0d2eeae75a1aa (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.lean14
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