summaryrefslogtreecommitdiff
path: root/tests/lean/Demo/Demo.lean
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean/Demo/Demo.lean')
-rw-r--r--tests/lean/Demo/Demo.lean32
1 files changed, 16 insertions, 16 deletions
diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
index 3a3aeb96..a9b349b3 100644
--- a/tests/lean/Demo/Demo.lean
+++ b/tests/lean/Demo/Demo.lean
@@ -6,7 +6,7 @@ open Primitives
namespace demo
/- [demo::choose]:
- Source: 'src/demo.rs', lines 5:0-5:70 -/
+ Source: 'tests/src/demo.rs', lines 5:0-5:70 -/
def choose
(T : Type) (b : Bool) (x : T) (y : T) :
Result (T × (T → Result (T × T)))
@@ -18,26 +18,26 @@ def choose
Result.ok (y, back)
/- [demo::mul2_add1]:
- Source: 'src/demo.rs', lines 13:0-13:31 -/
+ Source: 'tests/src/demo.rs', lines 13:0-13:31 -/
def mul2_add1 (x : U32) : Result U32 :=
do
let i ← x + x
i + 1#u32
/- [demo::use_mul2_add1]:
- Source: 'src/demo.rs', lines 17:0-17:43 -/
+ Source: 'tests/src/demo.rs', lines 17:0-17:43 -/
def use_mul2_add1 (x : U32) (y : U32) : Result U32 :=
do
let i ← mul2_add1 x
i + y
/- [demo::incr]:
- Source: 'src/demo.rs', lines 21:0-21:31 -/
+ Source: 'tests/src/demo.rs', lines 21:0-21:31 -/
def incr (x : U32) : Result U32 :=
x + 1#u32
/- [demo::use_incr]:
- Source: 'src/demo.rs', lines 25:0-25:17 -/
+ Source: 'tests/src/demo.rs', lines 25:0-25:17 -/
def use_incr : Result Unit :=
do
let x ← incr 0#u32
@@ -46,13 +46,13 @@ def use_incr : Result Unit :=
Result.ok ()
/- [demo::CList]
- Source: 'src/demo.rs', lines 34:0-34:17 -/
+ Source: 'tests/src/demo.rs', lines 34:0-34:17 -/
inductive CList (T : Type) :=
| CCons : T → CList T → CList T
| CNil : CList T
/- [demo::list_nth]:
- Source: 'src/demo.rs', lines 39:0-39:56 -/
+ Source: 'tests/src/demo.rs', lines 39:0-39:56 -/
divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T :=
match l with
| CList.CCons x tl =>
@@ -64,7 +64,7 @@ divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T :=
| CList.CNil => Result.fail .panic
/- [demo::list_nth_mut]:
- Source: 'src/demo.rs', lines 54:0-54:68 -/
+ Source: 'tests/src/demo.rs', lines 54:0-54:68 -/
divergent def list_nth_mut
(T : Type) (l : CList T) (i : U32) :
Result (T × (T → Result (CList T)))
@@ -88,7 +88,7 @@ divergent def list_nth_mut
| CList.CNil => Result.fail .panic
/- [demo::list_nth_mut1]: loop 0:
- Source: 'src/demo.rs', lines 69:0-78:1 -/
+ Source: 'tests/src/demo.rs', lines 69:0-78:1 -/
divergent def list_nth_mut1_loop
(T : Type) (l : CList T) (i : U32) :
Result (T × (T → Result (CList T)))
@@ -111,7 +111,7 @@ divergent def list_nth_mut1_loop
| CList.CNil => Result.fail .panic
/- [demo::list_nth_mut1]:
- Source: 'src/demo.rs', lines 69:0-69:77 -/
+ Source: 'tests/src/demo.rs', lines 69:0-69:77 -/
def list_nth_mut1
(T : Type) (l : CList T) (i : U32) :
Result (T × (T → Result (CList T)))
@@ -119,7 +119,7 @@ def list_nth_mut1
list_nth_mut1_loop T l i
/- [demo::i32_id]:
- Source: 'src/demo.rs', lines 80:0-80:28 -/
+ Source: 'tests/src/demo.rs', lines 80:0-80:28 -/
divergent def i32_id (i : I32) : Result I32 :=
if i = 0#i32
then Result.ok 0#i32
@@ -129,7 +129,7 @@ divergent def i32_id (i : I32) : Result I32 :=
i2 + 1#i32
/- [demo::list_tail]:
- Source: 'src/demo.rs', lines 88:0-88:64 -/
+ Source: 'tests/src/demo.rs', lines 88:0-88:64 -/
divergent def list_tail
(T : Type) (l : CList T) :
Result ((CList T) × (CList T → Result (CList T)))
@@ -147,25 +147,25 @@ divergent def list_tail
| CList.CNil => Result.ok (CList.CNil, Result.ok)
/- Trait declaration: [demo::Counter]
- Source: 'src/demo.rs', lines 97:0-97:17 -/
+ Source: 'tests/src/demo.rs', lines 97:0-97:17 -/
structure Counter (Self : Type) where
incr : Self → Result (Usize × Self)
/- [demo::{(demo::Counter for usize)}::incr]:
- Source: 'src/demo.rs', lines 102:4-102:31 -/
+ Source: 'tests/src/demo.rs', lines 102:4-102:31 -/
def CounterUsize.incr (self : Usize) : Result (Usize × Usize) :=
do
let self1 ← self + 1#usize
Result.ok (self, self1)
/- Trait implementation: [demo::{(demo::Counter for usize)}]
- Source: 'src/demo.rs', lines 101:0-101:22 -/
+ Source: 'tests/src/demo.rs', lines 101:0-101:22 -/
def CounterUsize : Counter Usize := {
incr := CounterUsize.incr
}
/- [demo::use_counter]:
- Source: 'src/demo.rs', lines 109:0-109:59 -/
+ Source: 'tests/src/demo.rs', lines 109:0-109:59 -/
def use_counter
(T : Type) (CounterInst : Counter T) (cnt : T) : Result (Usize × T) :=
CounterInst.incr cnt