summaryrefslogtreecommitdiff
path: root/tests/lean
diff options
context:
space:
mode:
authorAymeric Fromherz2024-05-24 15:02:26 +0200
committerAymeric Fromherz2024-05-24 15:02:26 +0200
commit4d33ea68ca1ebfca35b7d7332f63b74dd3c06838 (patch)
tree838da53ae7e5be27e1dde684d0354a5ce2a1fd99 /tests/lean
parentac5f261997079002a782217ebf0c854e31bb880d (diff)
parent3c8ea6df20f92be9c341bbfb748f65d6c598fead (diff)
Merge remote-tracking branch 'origin/main' into afromher_debug
Diffstat (limited to '')
-rw-r--r--tests/lean/Arrays.lean126
-rw-r--r--tests/lean/Bitwise.lean10
-rw-r--r--tests/lean/Constants.lean62
-rw-r--r--tests/lean/Demo/Demo.lean32
-rw-r--r--tests/lean/External/Funs.lean4
-rw-r--r--tests/lean/Hashmap/Funs.lean60
-rw-r--r--tests/lean/Hashmap/Types.lean4
-rw-r--r--tests/lean/HashmapMain/Funs.lean64
-rw-r--r--tests/lean/HashmapMain/FunsExternal_Template.lean4
-rw-r--r--tests/lean/HashmapMain/Types.lean4
-rw-r--r--tests/lean/Loops.lean98
-rw-r--r--tests/lean/NoNestedBorrows.lean126
-rw-r--r--tests/lean/Paper.lean18
-rw-r--r--tests/lean/PoloniusList.lean4
-rw-r--r--tests/lean/Traits.lean166
15 files changed, 391 insertions, 391 deletions
diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index d606640a..5ffcce51 100644
--- a/tests/lean/Arrays.lean
+++ b/tests/lean/Arrays.lean
@@ -6,24 +6,24 @@ open Primitives
namespace arrays
/- [arrays::AB]
- Source: 'src/arrays.rs', lines 3:0-3:11 -/
+ Source: 'tests/src/arrays.rs', lines 3:0-3:11 -/
inductive AB :=
| A : AB
| B : AB
/- [arrays::incr]:
- Source: 'src/arrays.rs', lines 8:0-8:24 -/
+ Source: 'tests/src/arrays.rs', lines 8:0-8:24 -/
def incr (x : U32) : Result U32 :=
x + 1#u32
/- [arrays::array_to_shared_slice_]:
- Source: 'src/arrays.rs', lines 16:0-16:53 -/
+ Source: 'tests/src/arrays.rs', lines 16:0-16:53 -/
def array_to_shared_slice_
(T : Type) (s : Array T 32#usize) : Result (Slice T) :=
Array.to_slice T 32#usize s
/- [arrays::array_to_mut_slice_]:
- Source: 'src/arrays.rs', lines 21:0-21:58 -/
+ Source: 'tests/src/arrays.rs', lines 21:0-21:58 -/
def array_to_mut_slice_
(T : Type) (s : Array T 32#usize) :
Result ((Slice T) × (Slice T → Result (Array T 32#usize)))
@@ -31,42 +31,42 @@ def array_to_mut_slice_
Array.to_slice_mut T 32#usize s
/- [arrays::array_len]:
- Source: 'src/arrays.rs', lines 25:0-25:40 -/
+ Source: 'tests/src/arrays.rs', lines 25:0-25:40 -/
def array_len (T : Type) (s : Array T 32#usize) : Result Usize :=
do
let s1 ← Array.to_slice T 32#usize s
Result.ok (Slice.len T s1)
/- [arrays::shared_array_len]:
- Source: 'src/arrays.rs', lines 29:0-29:48 -/
+ Source: 'tests/src/arrays.rs', lines 29:0-29:48 -/
def shared_array_len (T : Type) (s : Array T 32#usize) : Result Usize :=
do
let s1 ← Array.to_slice T 32#usize s
Result.ok (Slice.len T s1)
/- [arrays::shared_slice_len]:
- Source: 'src/arrays.rs', lines 33:0-33:44 -/
+ Source: 'tests/src/arrays.rs', lines 33:0-33:44 -/
def shared_slice_len (T : Type) (s : Slice T) : Result Usize :=
Result.ok (Slice.len T s)
/- [arrays::index_array_shared]:
- Source: 'src/arrays.rs', lines 37:0-37:57 -/
+ Source: 'tests/src/arrays.rs', lines 37:0-37:57 -/
def index_array_shared
(T : Type) (s : Array T 32#usize) (i : Usize) : Result T :=
Array.index_usize T 32#usize s i
/- [arrays::index_array_u32]:
- Source: 'src/arrays.rs', lines 44:0-44:53 -/
+ Source: 'tests/src/arrays.rs', lines 44:0-44:53 -/
def index_array_u32 (s : Array U32 32#usize) (i : Usize) : Result U32 :=
Array.index_usize U32 32#usize s i
/- [arrays::index_array_copy]:
- Source: 'src/arrays.rs', lines 48:0-48:45 -/
+ Source: 'tests/src/arrays.rs', lines 48:0-48:45 -/
def index_array_copy (x : Array U32 32#usize) : Result U32 :=
Array.index_usize U32 32#usize x 0#usize
/- [arrays::index_mut_array]:
- Source: 'src/arrays.rs', lines 52:0-52:62 -/
+ Source: 'tests/src/arrays.rs', lines 52:0-52:62 -/
def index_mut_array
(T : Type) (s : Array T 32#usize) (i : Usize) :
Result (T × (T → Result (Array T 32#usize)))
@@ -74,12 +74,12 @@ def index_mut_array
Array.index_mut_usize T 32#usize s i
/- [arrays::index_slice]:
- Source: 'src/arrays.rs', lines 56:0-56:46 -/
+ Source: 'tests/src/arrays.rs', lines 56:0-56:46 -/
def index_slice (T : Type) (s : Slice T) (i : Usize) : Result T :=
Slice.index_usize T s i
/- [arrays::index_mut_slice]:
- Source: 'src/arrays.rs', lines 60:0-60:58 -/
+ Source: 'tests/src/arrays.rs', lines 60:0-60:58 -/
def index_mut_slice
(T : Type) (s : Slice T) (i : Usize) :
Result (T × (T → Result (Slice T)))
@@ -87,7 +87,7 @@ def index_mut_slice
Slice.index_mut_usize T s i
/- [arrays::slice_subslice_shared_]:
- Source: 'src/arrays.rs', lines 64:0-64:70 -/
+ Source: 'tests/src/arrays.rs', lines 64:0-64:70 -/
def slice_subslice_shared_
(x : Slice U32) (y : Usize) (z : Usize) : Result (Slice U32) :=
core.slice.index.Slice.index U32 (core.ops.range.Range Usize)
@@ -95,7 +95,7 @@ def slice_subslice_shared_
{ start := y, end_ := z }
/- [arrays::slice_subslice_mut_]:
- Source: 'src/arrays.rs', lines 68:0-68:75 -/
+ Source: 'tests/src/arrays.rs', lines 68:0-68:75 -/
def slice_subslice_mut_
(x : Slice U32) (y : Usize) (z : Usize) :
Result ((Slice U32) × (Slice U32 → Result (Slice U32)))
@@ -108,12 +108,12 @@ def slice_subslice_mut_
Result.ok (s, index_mut_back)
/- [arrays::array_to_slice_shared_]:
- Source: 'src/arrays.rs', lines 72:0-72:54 -/
+ Source: 'tests/src/arrays.rs', lines 72:0-72:54 -/
def array_to_slice_shared_ (x : Array U32 32#usize) : Result (Slice U32) :=
Array.to_slice U32 32#usize x
/- [arrays::array_to_slice_mut_]:
- Source: 'src/arrays.rs', lines 76:0-76:59 -/
+ Source: 'tests/src/arrays.rs', lines 76:0-76:59 -/
def array_to_slice_mut_
(x : Array U32 32#usize) :
Result ((Slice U32) × (Slice U32 → Result (Array U32 32#usize)))
@@ -121,7 +121,7 @@ def array_to_slice_mut_
Array.to_slice_mut U32 32#usize x
/- [arrays::array_subslice_shared_]:
- Source: 'src/arrays.rs', lines 80:0-80:74 -/
+ Source: 'tests/src/arrays.rs', lines 80:0-80:74 -/
def array_subslice_shared_
(x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) :=
core.array.Array.index U32 (core.ops.range.Range Usize) 32#usize
@@ -130,7 +130,7 @@ def array_subslice_shared_
{ start := y, end_ := z }
/- [arrays::array_subslice_mut_]:
- Source: 'src/arrays.rs', lines 84:0-84:79 -/
+ Source: 'tests/src/arrays.rs', lines 84:0-84:79 -/
def array_subslice_mut_
(x : Array U32 32#usize) (y : Usize) (z : Usize) :
Result ((Slice U32) × (Slice U32 → Result (Array U32 32#usize)))
@@ -144,17 +144,17 @@ def array_subslice_mut_
Result.ok (s, index_mut_back)
/- [arrays::index_slice_0]:
- Source: 'src/arrays.rs', lines 88:0-88:38 -/
+ Source: 'tests/src/arrays.rs', lines 88:0-88:38 -/
def index_slice_0 (T : Type) (s : Slice T) : Result T :=
Slice.index_usize T s 0#usize
/- [arrays::index_array_0]:
- Source: 'src/arrays.rs', lines 92:0-92:42 -/
+ Source: 'tests/src/arrays.rs', lines 92:0-92:42 -/
def index_array_0 (T : Type) (s : Array T 32#usize) : Result T :=
Array.index_usize T 32#usize s 0#usize
/- [arrays::index_index_array]:
- Source: 'src/arrays.rs', lines 103:0-103:71 -/
+ Source: 'tests/src/arrays.rs', lines 103:0-103:71 -/
def index_index_array
(s : Array (Array U32 32#usize) 32#usize) (i : Usize) (j : Usize) :
Result U32
@@ -164,7 +164,7 @@ def index_index_array
Array.index_usize U32 32#usize a j
/- [arrays::update_update_array]:
- Source: 'src/arrays.rs', lines 114:0-114:70 -/
+ Source: 'tests/src/arrays.rs', lines 114:0-114:70 -/
def update_update_array
(s : Array (Array U32 32#usize) 32#usize) (i : Usize) (j : Usize) :
Result Unit
@@ -178,37 +178,37 @@ def update_update_array
Result.ok ()
/- [arrays::array_local_deep_copy]:
- Source: 'src/arrays.rs', lines 118:0-118:43 -/
+ Source: 'tests/src/arrays.rs', lines 118:0-118:43 -/
def array_local_deep_copy (x : Array U32 32#usize) : Result Unit :=
Result.ok ()
/- [arrays::take_array]:
- Source: 'src/arrays.rs', lines 122:0-122:30 -/
+ Source: 'tests/src/arrays.rs', lines 122:0-122:30 -/
def take_array (a : Array U32 2#usize) : Result Unit :=
Result.ok ()
/- [arrays::take_array_borrow]:
- Source: 'src/arrays.rs', lines 123:0-123:38 -/
+ Source: 'tests/src/arrays.rs', lines 123:0-123:38 -/
def take_array_borrow (a : Array U32 2#usize) : Result Unit :=
Result.ok ()
/- [arrays::take_slice]:
- Source: 'src/arrays.rs', lines 124:0-124:28 -/
+ Source: 'tests/src/arrays.rs', lines 124:0-124:28 -/
def take_slice (s : Slice U32) : Result Unit :=
Result.ok ()
/- [arrays::take_mut_slice]:
- Source: 'src/arrays.rs', lines 125:0-125:36 -/
+ Source: 'tests/src/arrays.rs', lines 125:0-125:36 -/
def take_mut_slice (s : Slice U32) : Result (Slice U32) :=
Result.ok s
/- [arrays::const_array]:
- Source: 'src/arrays.rs', lines 127:0-127:32 -/
+ Source: 'tests/src/arrays.rs', lines 127:0-127:32 -/
def const_array : Result (Array U32 2#usize) :=
Result.ok (Array.make U32 2#usize [ 0#u32, 0#u32 ])
/- [arrays::const_slice]:
- Source: 'src/arrays.rs', lines 131:0-131:20 -/
+ Source: 'tests/src/arrays.rs', lines 131:0-131:20 -/
def const_slice : Result Unit :=
do
let _ ←
@@ -216,7 +216,7 @@ def const_slice : Result Unit :=
Result.ok ()
/- [arrays::take_all]:
- Source: 'src/arrays.rs', lines 141:0-141:17 -/
+ Source: 'tests/src/arrays.rs', lines 141:0-141:17 -/
def take_all : Result Unit :=
do
let _ ← take_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
@@ -232,29 +232,29 @@ def take_all : Result Unit :=
Result.ok ()
/- [arrays::index_array]:
- Source: 'src/arrays.rs', lines 155:0-155:38 -/
+ Source: 'tests/src/arrays.rs', lines 155:0-155:38 -/
def index_array (x : Array U32 2#usize) : Result U32 :=
Array.index_usize U32 2#usize x 0#usize
/- [arrays::index_array_borrow]:
- Source: 'src/arrays.rs', lines 158:0-158:46 -/
+ Source: 'tests/src/arrays.rs', lines 158:0-158:46 -/
def index_array_borrow (x : Array U32 2#usize) : Result U32 :=
Array.index_usize U32 2#usize x 0#usize
/- [arrays::index_slice_u32_0]:
- Source: 'src/arrays.rs', lines 162:0-162:42 -/
+ Source: 'tests/src/arrays.rs', lines 162:0-162:42 -/
def index_slice_u32_0 (x : Slice U32) : Result U32 :=
Slice.index_usize U32 x 0#usize
/- [arrays::index_mut_slice_u32_0]:
- Source: 'src/arrays.rs', lines 166:0-166:50 -/
+ Source: 'tests/src/arrays.rs', lines 166:0-166:50 -/
def index_mut_slice_u32_0 (x : Slice U32) : Result (U32 × (Slice U32)) :=
do
let i ← Slice.index_usize U32 x 0#usize
Result.ok (i, x)
/- [arrays::index_all]:
- Source: 'src/arrays.rs', lines 170:0-170:25 -/
+ Source: 'tests/src/arrays.rs', lines 170:0-170:25 -/
def index_all : Result U32 :=
do
let i ← index_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
@@ -274,7 +274,7 @@ def index_all : Result U32 :=
Result.ok i8
/- [arrays::update_array]:
- Source: 'src/arrays.rs', lines 184:0-184:36 -/
+ Source: 'tests/src/arrays.rs', lines 184:0-184:36 -/
def update_array (x : Array U32 2#usize) : Result Unit :=
do
let (_, index_mut_back) ← Array.index_mut_usize U32 2#usize x 0#usize
@@ -282,7 +282,7 @@ def update_array (x : Array U32 2#usize) : Result Unit :=
Result.ok ()
/- [arrays::update_array_mut_borrow]:
- Source: 'src/arrays.rs', lines 187:0-187:48 -/
+ Source: 'tests/src/arrays.rs', lines 187:0-187:48 -/
def update_array_mut_borrow
(x : Array U32 2#usize) : Result (Array U32 2#usize) :=
do
@@ -290,14 +290,14 @@ def update_array_mut_borrow
index_mut_back 1#u32
/- [arrays::update_mut_slice]:
- Source: 'src/arrays.rs', lines 190:0-190:38 -/
+ Source: 'tests/src/arrays.rs', lines 190:0-190:38 -/
def update_mut_slice (x : Slice U32) : Result (Slice U32) :=
do
let (_, index_mut_back) ← Slice.index_mut_usize U32 x 0#usize
index_mut_back 1#u32
/- [arrays::update_all]:
- Source: 'src/arrays.rs', lines 194:0-194:19 -/
+ Source: 'tests/src/arrays.rs', lines 194:0-194:19 -/
def update_all : Result Unit :=
do
let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
@@ -309,7 +309,7 @@ def update_all : Result Unit :=
Result.ok ()
/- [arrays::range_all]:
- Source: 'src/arrays.rs', lines 205:0-205:18 -/
+ Source: 'tests/src/arrays.rs', lines 205:0-205:18 -/
def range_all : Result Unit :=
do
let (s, index_mut_back) ←
@@ -323,12 +323,12 @@ def range_all : Result Unit :=
Result.ok ()
/- [arrays::deref_array_borrow]:
- Source: 'src/arrays.rs', lines 214:0-214:46 -/
+ Source: 'tests/src/arrays.rs', lines 214:0-214:46 -/
def deref_array_borrow (x : Array U32 2#usize) : Result U32 :=
Array.index_usize U32 2#usize x 0#usize
/- [arrays::deref_array_mut_borrow]:
- Source: 'src/arrays.rs', lines 219:0-219:54 -/
+ Source: 'tests/src/arrays.rs', lines 219:0-219:54 -/
def deref_array_mut_borrow
(x : Array U32 2#usize) : Result (U32 × (Array U32 2#usize)) :=
do
@@ -336,17 +336,17 @@ def deref_array_mut_borrow
Result.ok (i, x)
/- [arrays::take_array_t]:
- Source: 'src/arrays.rs', lines 227:0-227:31 -/
+ Source: 'tests/src/arrays.rs', lines 227:0-227:31 -/
def take_array_t (a : Array AB 2#usize) : Result Unit :=
Result.ok ()
/- [arrays::non_copyable_array]:
- Source: 'src/arrays.rs', lines 229:0-229:27 -/
+ Source: 'tests/src/arrays.rs', lines 229:0-229:27 -/
def non_copyable_array : Result Unit :=
take_array_t (Array.make AB 2#usize [ AB.A, AB.B ])
/- [arrays::sum]: loop 0:
- Source: 'src/arrays.rs', lines 242:0-250:1 -/
+ Source: 'tests/src/arrays.rs', lines 242:0-250:1 -/
divergent def sum_loop (s : Slice U32) (sum1 : U32) (i : Usize) : Result U32 :=
let i1 := Slice.len U32 s
if i < i1
@@ -359,12 +359,12 @@ divergent def sum_loop (s : Slice U32) (sum1 : U32) (i : Usize) : Result U32 :=
else Result.ok sum1
/- [arrays::sum]:
- Source: 'src/arrays.rs', lines 242:0-242:28 -/
+ Source: 'tests/src/arrays.rs', lines 242:0-242:28 -/
def sum (s : Slice U32) : Result U32 :=
sum_loop s 0#u32 0#usize
/- [arrays::sum2]: loop 0:
- Source: 'src/arrays.rs', lines 252:0-261:1 -/
+ Source: 'tests/src/arrays.rs', lines 252:0-261:1 -/
divergent def sum2_loop
(s : Slice U32) (s2 : Slice U32) (sum1 : U32) (i : Usize) : Result U32 :=
let i1 := Slice.len U32 s
@@ -380,7 +380,7 @@ divergent def sum2_loop
else Result.ok sum1
/- [arrays::sum2]:
- Source: 'src/arrays.rs', lines 252:0-252:41 -/
+ Source: 'tests/src/arrays.rs', lines 252:0-252:41 -/
def sum2 (s : Slice U32) (s2 : Slice U32) : Result U32 :=
let i := Slice.len U32 s
let i1 := Slice.len U32 s2
@@ -389,7 +389,7 @@ def sum2 (s : Slice U32) (s2 : Slice U32) : Result U32 :=
else sum2_loop s s2 0#u32 0#usize
/- [arrays::f0]:
- Source: 'src/arrays.rs', lines 263:0-263:11 -/
+ Source: 'tests/src/arrays.rs', lines 263:0-263:11 -/
def f0 : Result Unit :=
do
let (s, to_slice_mut_back) ←
@@ -400,7 +400,7 @@ def f0 : Result Unit :=
Result.ok ()
/- [arrays::f1]:
- Source: 'src/arrays.rs', lines 268:0-268:11 -/
+ Source: 'tests/src/arrays.rs', lines 268:0-268:11 -/
def f1 : Result Unit :=
do
let (_, index_mut_back) ←
@@ -410,12 +410,12 @@ def f1 : Result Unit :=
Result.ok ()
/- [arrays::f2]:
- Source: 'src/arrays.rs', lines 273:0-273:17 -/
+ Source: 'tests/src/arrays.rs', lines 273:0-273:17 -/
def f2 (i : U32) : Result Unit :=
Result.ok ()
/- [arrays::f4]:
- Source: 'src/arrays.rs', lines 282:0-282:54 -/
+ Source: 'tests/src/arrays.rs', lines 282:0-282:54 -/
def f4 (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) :=
core.array.Array.index U32 (core.ops.range.Range Usize) 32#usize
(core.ops.index.IndexSliceTIInst U32 (core.ops.range.Range Usize)
@@ -423,7 +423,7 @@ def f4 (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) :=
{ start := y, end_ := z }
/- [arrays::f3]:
- Source: 'src/arrays.rs', lines 275:0-275:18 -/
+ Source: 'tests/src/arrays.rs', lines 275:0-275:18 -/
def f3 : Result U32 :=
do
let i ←
@@ -437,17 +437,17 @@ def f3 : Result U32 :=
sum2 s s1
/- [arrays::SZ]
- Source: 'src/arrays.rs', lines 286:0-286:19 -/
+ Source: 'tests/src/arrays.rs', lines 286:0-286:19 -/
def SZ_body : Result Usize := Result.ok 32#usize
def SZ : Usize := eval_global SZ_body
/- [arrays::f5]:
- Source: 'src/arrays.rs', lines 289:0-289:31 -/
+ Source: 'tests/src/arrays.rs', lines 289:0-289:31 -/
def f5 (x : Array U32 32#usize) : Result U32 :=
Array.index_usize U32 32#usize x 0#usize
/- [arrays::ite]:
- Source: 'src/arrays.rs', lines 294:0-294:12 -/
+ Source: 'tests/src/arrays.rs', lines 294:0-294:12 -/
def ite : Result Unit :=
do
let (s, to_slice_mut_back) ←
@@ -461,7 +461,7 @@ def ite : Result Unit :=
Result.ok ()
/- [arrays::zero_slice]: loop 0:
- Source: 'src/arrays.rs', lines 303:0-310:1 -/
+ Source: 'tests/src/arrays.rs', lines 303:0-310:1 -/
divergent def zero_slice_loop
(a : Slice U8) (i : Usize) (len : Usize) : Result (Slice U8) :=
if i < len
@@ -474,13 +474,13 @@ divergent def zero_slice_loop
else Result.ok a
/- [arrays::zero_slice]:
- Source: 'src/arrays.rs', lines 303:0-303:31 -/
+ Source: 'tests/src/arrays.rs', lines 303:0-303:31 -/
def zero_slice (a : Slice U8) : Result (Slice U8) :=
let len := Slice.len U8 a
zero_slice_loop a 0#usize len
/- [arrays::iter_mut_slice]: loop 0:
- Source: 'src/arrays.rs', lines 312:0-318:1 -/
+ Source: 'tests/src/arrays.rs', lines 312:0-318:1 -/
divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit :=
if i < len
then do
@@ -489,7 +489,7 @@ divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit :=
else Result.ok ()
/- [arrays::iter_mut_slice]:
- Source: 'src/arrays.rs', lines 312:0-312:35 -/
+ Source: 'tests/src/arrays.rs', lines 312:0-312:35 -/
def iter_mut_slice (a : Slice U8) : Result (Slice U8) :=
do
let len := Slice.len U8 a
@@ -497,7 +497,7 @@ def iter_mut_slice (a : Slice U8) : Result (Slice U8) :=
Result.ok a
/- [arrays::sum_mut_slice]: loop 0:
- Source: 'src/arrays.rs', lines 320:0-328:1 -/
+ Source: 'tests/src/arrays.rs', lines 320:0-328:1 -/
divergent def sum_mut_slice_loop
(a : Slice U32) (i : Usize) (s : U32) : Result U32 :=
let i1 := Slice.len U32 a
@@ -511,7 +511,7 @@ divergent def sum_mut_slice_loop
else Result.ok s
/- [arrays::sum_mut_slice]:
- Source: 'src/arrays.rs', lines 320:0-320:42 -/
+ Source: 'tests/src/arrays.rs', lines 320:0-320:42 -/
def sum_mut_slice (a : Slice U32) : Result (U32 × (Slice U32)) :=
do
let i ← sum_mut_slice_loop a 0#usize 0#u32
diff --git a/tests/lean/Bitwise.lean b/tests/lean/Bitwise.lean
index c13129f1..4ed56a0a 100644
--- a/tests/lean/Bitwise.lean
+++ b/tests/lean/Bitwise.lean
@@ -6,31 +6,31 @@ open Primitives
namespace bitwise
/- [bitwise::shift_u32]:
- Source: 'src/bitwise.rs', lines 3:0-3:31 -/
+ Source: 'tests/src/bitwise.rs', lines 3:0-3:31 -/
def shift_u32 (a : U32) : Result U32 :=
do
let t ← a >>> 16#usize
t <<< 16#usize
/- [bitwise::shift_i32]:
- Source: 'src/bitwise.rs', lines 10:0-10:31 -/
+ Source: 'tests/src/bitwise.rs', lines 10:0-10:31 -/
def shift_i32 (a : I32) : Result I32 :=
do
let t ← a >>> 16#isize
t <<< 16#isize
/- [bitwise::xor_u32]:
- Source: 'src/bitwise.rs', lines 17:0-17:37 -/
+ Source: 'tests/src/bitwise.rs', lines 17:0-17:37 -/
def xor_u32 (a : U32) (b : U32) : Result U32 :=
Result.ok (a ^^^ b)
/- [bitwise::or_u32]:
- Source: 'src/bitwise.rs', lines 21:0-21:36 -/
+ Source: 'tests/src/bitwise.rs', lines 21:0-21:36 -/
def or_u32 (a : U32) (b : U32) : Result U32 :=
Result.ok (a ||| b)
/- [bitwise::and_u32]:
- Source: 'src/bitwise.rs', lines 25:0-25:37 -/
+ Source: 'tests/src/bitwise.rs', lines 25:0-25:37 -/
def and_u32 (a : U32) (b : U32) : Result U32 :=
Result.ok (a &&& b)
diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean
index 3cc3ca40..532f265a 100644
--- a/tests/lean/Constants.lean
+++ b/tests/lean/Constants.lean
@@ -6,123 +6,123 @@ open Primitives
namespace constants
/- [constants::X0]
- Source: 'src/constants.rs', lines 5:0-5:17 -/
+ Source: 'tests/src/constants.rs', lines 5:0-5:17 -/
def X0_body : Result U32 := Result.ok 0#u32
def X0 : U32 := eval_global X0_body
/- [constants::X1]
- Source: 'src/constants.rs', lines 7:0-7:17 -/
+ Source: 'tests/src/constants.rs', lines 7:0-7:17 -/
def X1_body : Result U32 := Result.ok core_u32_max
def X1 : U32 := eval_global X1_body
/- [constants::X2]
- Source: 'src/constants.rs', lines 10:0-10:17 -/
+ Source: 'tests/src/constants.rs', lines 10:0-10:17 -/
def X2_body : Result U32 := Result.ok 3#u32
def X2 : U32 := eval_global X2_body
/- [constants::incr]:
- Source: 'src/constants.rs', lines 17:0-17:32 -/
+ Source: 'tests/src/constants.rs', lines 17:0-17:32 -/
def incr (n : U32) : Result U32 :=
n + 1#u32
/- [constants::X3]
- Source: 'src/constants.rs', lines 15:0-15:17 -/
+ Source: 'tests/src/constants.rs', lines 15:0-15:17 -/
def X3_body : Result U32 := incr 32#u32
def X3 : U32 := eval_global X3_body
/- [constants::mk_pair0]:
- Source: 'src/constants.rs', lines 23:0-23:51 -/
+ Source: 'tests/src/constants.rs', lines 23:0-23:51 -/
def mk_pair0 (x : U32) (y : U32) : Result (U32 × U32) :=
Result.ok (x, y)
/- [constants::Pair]
- Source: 'src/constants.rs', lines 36:0-36:23 -/
+ Source: 'tests/src/constants.rs', lines 36:0-36:23 -/
structure Pair (T1 T2 : Type) where
x : T1
y : T2
/- [constants::mk_pair1]:
- Source: 'src/constants.rs', lines 27:0-27:55 -/
+ Source: 'tests/src/constants.rs', lines 27:0-27:55 -/
def mk_pair1 (x : U32) (y : U32) : Result (Pair U32 U32) :=
Result.ok { x := x, y := y }
/- [constants::P0]
- Source: 'src/constants.rs', lines 31:0-31:24 -/
+ Source: 'tests/src/constants.rs', lines 31:0-31:24 -/
def P0_body : Result (U32 × U32) := mk_pair0 0#u32 1#u32
def P0 : (U32 × U32) := eval_global P0_body
/- [constants::P1]
- Source: 'src/constants.rs', lines 32:0-32:28 -/
+ Source: 'tests/src/constants.rs', lines 32:0-32:28 -/
def P1_body : Result (Pair U32 U32) := mk_pair1 0#u32 1#u32
def P1 : Pair U32 U32 := eval_global P1_body
/- [constants::P2]
- Source: 'src/constants.rs', lines 33:0-33:24 -/
+ Source: 'tests/src/constants.rs', lines 33:0-33:24 -/
def P2_body : Result (U32 × U32) := Result.ok (0#u32, 1#u32)
def P2 : (U32 × U32) := eval_global P2_body
/- [constants::P3]
- Source: 'src/constants.rs', lines 34:0-34:28 -/
+ Source: 'tests/src/constants.rs', lines 34:0-34:28 -/
def P3_body : Result (Pair U32 U32) := Result.ok { x := 0#u32, y := 1#u32 }
def P3 : Pair U32 U32 := eval_global P3_body
/- [constants::Wrap]
- Source: 'src/constants.rs', lines 49:0-49:18 -/
+ Source: 'tests/src/constants.rs', lines 49:0-49:18 -/
structure Wrap (T : Type) where
value : T
/- [constants::{constants::Wrap<T>}::new]:
- Source: 'src/constants.rs', lines 54:4-54:41 -/
+ Source: 'tests/src/constants.rs', lines 54:4-54:41 -/
def Wrap.new (T : Type) (value : T) : Result (Wrap T) :=
Result.ok { value := value }
/- [constants::Y]
- Source: 'src/constants.rs', lines 41:0-41:22 -/
+ Source: 'tests/src/constants.rs', lines 41:0-41:22 -/
def Y_body : Result (Wrap I32) := Wrap.new I32 2#i32
def Y : Wrap I32 := eval_global Y_body
/- [constants::unwrap_y]:
- Source: 'src/constants.rs', lines 43:0-43:30 -/
+ Source: 'tests/src/constants.rs', lines 43:0-43:30 -/
def unwrap_y : Result I32 :=
Result.ok Y.value
/- [constants::YVAL]
- Source: 'src/constants.rs', lines 47:0-47:19 -/
+ Source: 'tests/src/constants.rs', lines 47:0-47:19 -/
def YVAL_body : Result I32 := unwrap_y
def YVAL : I32 := eval_global YVAL_body
/- [constants::get_z1::Z1]
- Source: 'src/constants.rs', lines 62:4-62:17 -/
+ Source: 'tests/src/constants.rs', lines 62:4-62:17 -/
def get_z1.Z1_body : Result I32 := Result.ok 3#i32
def get_z1.Z1 : I32 := eval_global get_z1.Z1_body
/- [constants::get_z1]:
- Source: 'src/constants.rs', lines 61:0-61:28 -/
+ Source: 'tests/src/constants.rs', lines 61:0-61:28 -/
def get_z1 : Result I32 :=
Result.ok get_z1.Z1
/- [constants::add]:
- Source: 'src/constants.rs', lines 66:0-66:39 -/
+ Source: 'tests/src/constants.rs', lines 66:0-66:39 -/
def add (a : I32) (b : I32) : Result I32 :=
a + b
/- [constants::Q1]
- Source: 'src/constants.rs', lines 74:0-74:17 -/
+ Source: 'tests/src/constants.rs', lines 74:0-74:17 -/
def Q1_body : Result I32 := Result.ok 5#i32
def Q1 : I32 := eval_global Q1_body
/- [constants::Q2]
- Source: 'src/constants.rs', lines 75:0-75:17 -/
+ Source: 'tests/src/constants.rs', lines 75:0-75:17 -/
def Q2_body : Result I32 := Result.ok Q1
def Q2 : I32 := eval_global Q2_body
/- [constants::Q3]
- Source: 'src/constants.rs', lines 76:0-76:17 -/
+ Source: 'tests/src/constants.rs', lines 76:0-76:17 -/
def Q3_body : Result I32 := add Q2 3#i32
def Q3 : I32 := eval_global Q3_body
/- [constants::get_z2]:
- Source: 'src/constants.rs', lines 70:0-70:28 -/
+ Source: 'tests/src/constants.rs', lines 70:0-70:28 -/
def get_z2 : Result I32 :=
do
let i ← get_z1
@@ -130,37 +130,37 @@ def get_z2 : Result I32 :=
add Q1 i1
/- [constants::S1]
- Source: 'src/constants.rs', lines 80:0-80:18 -/
+ Source: 'tests/src/constants.rs', lines 80:0-80:18 -/
def S1_body : Result U32 := Result.ok 6#u32
def S1 : U32 := eval_global S1_body
/- [constants::S2]
- Source: 'src/constants.rs', lines 81:0-81:18 -/
+ Source: 'tests/src/constants.rs', lines 81:0-81:18 -/
def S2_body : Result U32 := incr S1
def S2 : U32 := eval_global S2_body
/- [constants::S3]
- Source: 'src/constants.rs', lines 82:0-82:29 -/
+ Source: 'tests/src/constants.rs', lines 82:0-82:29 -/
def S3_body : Result (Pair U32 U32) := Result.ok P3
def S3 : Pair U32 U32 := eval_global S3_body
/- [constants::S4]
- Source: 'src/constants.rs', lines 83:0-83:29 -/
+ Source: 'tests/src/constants.rs', lines 83:0-83:29 -/
def S4_body : Result (Pair U32 U32) := mk_pair1 7#u32 8#u32
def S4 : Pair U32 U32 := eval_global S4_body
/- [constants::V]
- Source: 'src/constants.rs', lines 86:0-86:31 -/
+ Source: 'tests/src/constants.rs', lines 86:0-86:31 -/
structure V (T : Type) (N : Usize) where
x : Array T N
/- [constants::{constants::V<T, N>#1}::LEN]
- Source: 'src/constants.rs', lines 91:4-91:24 -/
+ Source: 'tests/src/constants.rs', lines 91:4-91:24 -/
def V.LEN_body (T : Type) (N : Usize) : Result Usize := Result.ok N
def V.LEN (T : Type) (N : Usize) : Usize := eval_global (V.LEN_body T N)
/- [constants::use_v]:
- Source: 'src/constants.rs', lines 94:0-94:42 -/
+ Source: 'tests/src/constants.rs', lines 94:0-94:42 -/
def use_v (T : Type) (N : Usize) : Result Usize :=
Result.ok (V.LEN T N)
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
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index 0b0a2476..5e3c9b1d 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -15,12 +15,12 @@ def core.marker.CopyU32 : core.marker.Copy U32 := {
}
/- [external::use_get]:
- Source: 'src/external.rs', lines 5:0-5:37 -/
+ Source: 'tests/src/external.rs', lines 5:0-5:37 -/
def use_get (rc : core.cell.Cell U32) (st : State) : Result (State × U32) :=
core.cell.Cell.get U32 core.marker.CopyU32 rc st
/- [external::incr]:
- Source: 'src/external.rs', lines 9:0-9:31 -/
+ Source: 'tests/src/external.rs', lines 9:0-9:31 -/
def incr
(rc : core.cell.Cell U32) (st : State) :
Result (State × (core.cell.Cell U32))
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 9cbd958c..cb11e5cf 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -7,12 +7,12 @@ open Primitives
namespace hashmap
/- [hashmap::hash_key]:
- Source: 'src/hashmap.rs', lines 27:0-27:32 -/
+ Source: 'tests/src/hashmap.rs', lines 27:0-27:32 -/
def hash_key (k : Usize) : Result Usize :=
Result.ok k
/- [hashmap::{hashmap::HashMap<T>}::allocate_slots]: loop 0:
- Source: 'src/hashmap.rs', lines 50:4-56:5 -/
+ Source: 'tests/src/hashmap.rs', lines 50:4-56:5 -/
divergent def HashMap.allocate_slots_loop
(T : Type) (slots : alloc.vec.Vec (List T)) (n : Usize) :
Result (alloc.vec.Vec (List T))
@@ -26,7 +26,7 @@ divergent def HashMap.allocate_slots_loop
else Result.ok slots
/- [hashmap::{hashmap::HashMap<T>}::allocate_slots]:
- Source: 'src/hashmap.rs', lines 50:4-50:76 -/
+ Source: 'tests/src/hashmap.rs', lines 50:4-50:76 -/
def HashMap.allocate_slots
(T : Type) (slots : alloc.vec.Vec (List T)) (n : Usize) :
Result (alloc.vec.Vec (List T))
@@ -34,7 +34,7 @@ def HashMap.allocate_slots
HashMap.allocate_slots_loop T slots n
/- [hashmap::{hashmap::HashMap<T>}::new_with_capacity]:
- Source: 'src/hashmap.rs', lines 59:4-63:13 -/
+ Source: 'tests/src/hashmap.rs', lines 59:4-63:13 -/
def HashMap.new_with_capacity
(T : Type) (capacity : Usize) (max_load_dividend : Usize)
(max_load_divisor : Usize) :
@@ -53,12 +53,12 @@ def HashMap.new_with_capacity
}
/- [hashmap::{hashmap::HashMap<T>}::new]:
- Source: 'src/hashmap.rs', lines 75:4-75:24 -/
+ Source: 'tests/src/hashmap.rs', lines 75:4-75:24 -/
def HashMap.new (T : Type) : Result (HashMap T) :=
HashMap.new_with_capacity T 32#usize 4#usize 5#usize
/- [hashmap::{hashmap::HashMap<T>}::clear]: loop 0:
- Source: 'src/hashmap.rs', lines 80:4-88:5 -/
+ Source: 'tests/src/hashmap.rs', lines 80:4-88:5 -/
divergent def HashMap.clear_loop
(T : Type) (slots : alloc.vec.Vec (List T)) (i : Usize) :
Result (alloc.vec.Vec (List T))
@@ -76,19 +76,19 @@ divergent def HashMap.clear_loop
else Result.ok slots
/- [hashmap::{hashmap::HashMap<T>}::clear]:
- Source: 'src/hashmap.rs', lines 80:4-80:27 -/
+ Source: 'tests/src/hashmap.rs', lines 80:4-80:27 -/
def HashMap.clear (T : Type) (self : HashMap T) : Result (HashMap T) :=
do
let hm ← HashMap.clear_loop T self.slots 0#usize
Result.ok { self with num_entries := 0#usize, slots := hm }
/- [hashmap::{hashmap::HashMap<T>}::len]:
- Source: 'src/hashmap.rs', lines 90:4-90:30 -/
+ Source: 'tests/src/hashmap.rs', lines 90:4-90:30 -/
def HashMap.len (T : Type) (self : HashMap T) : Result Usize :=
Result.ok self.num_entries
/- [hashmap::{hashmap::HashMap<T>}::insert_in_list]: loop 0:
- Source: 'src/hashmap.rs', lines 97:4-114:5 -/
+ Source: 'tests/src/hashmap.rs', lines 97:4-114:5 -/
divergent def HashMap.insert_in_list_loop
(T : Type) (key : Usize) (value : T) (ls : List T) :
Result (Bool × (List T))
@@ -104,7 +104,7 @@ divergent def HashMap.insert_in_list_loop
| List.Nil => Result.ok (true, List.Cons key value List.Nil)
/- [hashmap::{hashmap::HashMap<T>}::insert_in_list]:
- Source: 'src/hashmap.rs', lines 97:4-97:71 -/
+ Source: 'tests/src/hashmap.rs', lines 97:4-97:71 -/
def HashMap.insert_in_list
(T : Type) (key : Usize) (value : T) (ls : List T) :
Result (Bool × (List T))
@@ -112,7 +112,7 @@ def HashMap.insert_in_list
HashMap.insert_in_list_loop T key value ls
/- [hashmap::{hashmap::HashMap<T>}::insert_no_resize]:
- Source: 'src/hashmap.rs', lines 117:4-117:54 -/
+ Source: 'tests/src/hashmap.rs', lines 117:4-117:54 -/
def HashMap.insert_no_resize
(T : Type) (self : HashMap T) (key : Usize) (value : T) :
Result (HashMap T)
@@ -136,7 +136,7 @@ def HashMap.insert_no_resize
Result.ok { self with slots := v }
/- [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]: loop 0:
- Source: 'src/hashmap.rs', lines 183:4-196:5 -/
+ Source: 'tests/src/hashmap.rs', lines 183:4-196:5 -/
divergent def HashMap.move_elements_from_list_loop
(T : Type) (ntable : HashMap T) (ls : List T) : Result (HashMap T) :=
match ls with
@@ -147,13 +147,13 @@ divergent def HashMap.move_elements_from_list_loop
| List.Nil => Result.ok ntable
/- [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]:
- Source: 'src/hashmap.rs', lines 183:4-183:72 -/
+ Source: 'tests/src/hashmap.rs', lines 183:4-183:72 -/
def HashMap.move_elements_from_list
(T : Type) (ntable : HashMap T) (ls : List T) : Result (HashMap T) :=
HashMap.move_elements_from_list_loop T ntable ls
/- [hashmap::{hashmap::HashMap<T>}::move_elements]: loop 0:
- Source: 'src/hashmap.rs', lines 171:4-180:5 -/
+ Source: 'tests/src/hashmap.rs', lines 171:4-180:5 -/
divergent def HashMap.move_elements_loop
(T : Type) (ntable : HashMap T) (slots : alloc.vec.Vec (List T)) (i : Usize)
:
@@ -174,7 +174,7 @@ divergent def HashMap.move_elements_loop
else Result.ok (ntable, slots)
/- [hashmap::{hashmap::HashMap<T>}::move_elements]:
- Source: 'src/hashmap.rs', lines 171:4-171:95 -/
+ Source: 'tests/src/hashmap.rs', lines 171:4-171:95 -/
def HashMap.move_elements
(T : Type) (ntable : HashMap T) (slots : alloc.vec.Vec (List T)) (i : Usize)
:
@@ -183,7 +183,7 @@ def HashMap.move_elements
HashMap.move_elements_loop T ntable slots i
/- [hashmap::{hashmap::HashMap<T>}::try_resize]:
- Source: 'src/hashmap.rs', lines 140:4-140:28 -/
+ Source: 'tests/src/hashmap.rs', lines 140:4-140:28 -/
def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) :=
do
let max_usize ← Scalar.cast .Usize core_u32_max
@@ -207,7 +207,7 @@ def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) :=
else Result.ok { self with max_load_factor := (i, i1) }
/- [hashmap::{hashmap::HashMap<T>}::insert]:
- Source: 'src/hashmap.rs', lines 129:4-129:48 -/
+ Source: 'tests/src/hashmap.rs', lines 129:4-129:48 -/
def HashMap.insert
(T : Type) (self : HashMap T) (key : Usize) (value : T) :
Result (HashMap T)
@@ -220,7 +220,7 @@ def HashMap.insert
else Result.ok self1
/- [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
- Source: 'src/hashmap.rs', lines 206:4-219:5 -/
+ Source: 'tests/src/hashmap.rs', lines 206:4-219:5 -/
divergent def HashMap.contains_key_in_list_loop
(T : Type) (key : Usize) (ls : List T) : Result Bool :=
match ls with
@@ -231,13 +231,13 @@ divergent def HashMap.contains_key_in_list_loop
| List.Nil => Result.ok false
/- [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]:
- Source: 'src/hashmap.rs', lines 206:4-206:68 -/
+ Source: 'tests/src/hashmap.rs', lines 206:4-206:68 -/
def HashMap.contains_key_in_list
(T : Type) (key : Usize) (ls : List T) : Result Bool :=
HashMap.contains_key_in_list_loop T key ls
/- [hashmap::{hashmap::HashMap<T>}::contains_key]:
- Source: 'src/hashmap.rs', lines 199:4-199:49 -/
+ Source: 'tests/src/hashmap.rs', lines 199:4-199:49 -/
def HashMap.contains_key
(T : Type) (self : HashMap T) (key : Usize) : Result Bool :=
do
@@ -250,7 +250,7 @@ def HashMap.contains_key
HashMap.contains_key_in_list T key l
/- [hashmap::{hashmap::HashMap<T>}::get_in_list]: loop 0:
- Source: 'src/hashmap.rs', lines 224:4-237:5 -/
+ Source: 'tests/src/hashmap.rs', lines 224:4-237:5 -/
divergent def HashMap.get_in_list_loop
(T : Type) (key : Usize) (ls : List T) : Result T :=
match ls with
@@ -261,12 +261,12 @@ divergent def HashMap.get_in_list_loop
| List.Nil => Result.fail .panic
/- [hashmap::{hashmap::HashMap<T>}::get_in_list]:
- Source: 'src/hashmap.rs', lines 224:4-224:70 -/
+ Source: 'tests/src/hashmap.rs', lines 224:4-224:70 -/
def HashMap.get_in_list (T : Type) (key : Usize) (ls : List T) : Result T :=
HashMap.get_in_list_loop T key ls
/- [hashmap::{hashmap::HashMap<T>}::get]:
- Source: 'src/hashmap.rs', lines 239:4-239:55 -/
+ Source: 'tests/src/hashmap.rs', lines 239:4-239:55 -/
def HashMap.get (T : Type) (self : HashMap T) (key : Usize) : Result T :=
do
let hash ← hash_key key
@@ -278,7 +278,7 @@ def HashMap.get (T : Type) (self : HashMap T) (key : Usize) : Result T :=
HashMap.get_in_list T key l
/- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]: loop 0:
- Source: 'src/hashmap.rs', lines 245:4-254:5 -/
+ Source: 'tests/src/hashmap.rs', lines 245:4-254:5 -/
divergent def HashMap.get_mut_in_list_loop
(T : Type) (ls : List T) (key : Usize) :
Result (T × (T → Result (List T)))
@@ -301,7 +301,7 @@ divergent def HashMap.get_mut_in_list_loop
| List.Nil => Result.fail .panic
/- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]:
- Source: 'src/hashmap.rs', lines 245:4-245:86 -/
+ Source: 'tests/src/hashmap.rs', lines 245:4-245:86 -/
def HashMap.get_mut_in_list
(T : Type) (ls : List T) (key : Usize) :
Result (T × (T → Result (List T)))
@@ -309,7 +309,7 @@ def HashMap.get_mut_in_list
HashMap.get_mut_in_list_loop T ls key
/- [hashmap::{hashmap::HashMap<T>}::get_mut]:
- Source: 'src/hashmap.rs', lines 257:4-257:67 -/
+ Source: 'tests/src/hashmap.rs', lines 257:4-257:67 -/
def HashMap.get_mut
(T : Type) (self : HashMap T) (key : Usize) :
Result (T × (T → Result (HashMap T)))
@@ -331,7 +331,7 @@ def HashMap.get_mut
Result.ok (t, back)
/- [hashmap::{hashmap::HashMap<T>}::remove_from_list]: loop 0:
- Source: 'src/hashmap.rs', lines 265:4-291:5 -/
+ Source: 'tests/src/hashmap.rs', lines 265:4-291:5 -/
divergent def HashMap.remove_from_list_loop
(T : Type) (key : Usize) (ls : List T) : Result ((Option T) × (List T)) :=
match ls with
@@ -350,13 +350,13 @@ divergent def HashMap.remove_from_list_loop
| List.Nil => Result.ok (none, List.Nil)
/- [hashmap::{hashmap::HashMap<T>}::remove_from_list]:
- Source: 'src/hashmap.rs', lines 265:4-265:69 -/
+ Source: 'tests/src/hashmap.rs', lines 265:4-265:69 -/
def HashMap.remove_from_list
(T : Type) (key : Usize) (ls : List T) : Result ((Option T) × (List T)) :=
HashMap.remove_from_list_loop T key ls
/- [hashmap::{hashmap::HashMap<T>}::remove]:
- Source: 'src/hashmap.rs', lines 294:4-294:52 -/
+ Source: 'tests/src/hashmap.rs', lines 294:4-294:52 -/
def HashMap.remove
(T : Type) (self : HashMap T) (key : Usize) :
Result ((Option T) × (HashMap T))
@@ -381,7 +381,7 @@ def HashMap.remove
Result.ok (some x1, { self with num_entries := i1, slots := v })
/- [hashmap::test1]:
- Source: 'src/hashmap.rs', lines 315:0-315:10 -/
+ Source: 'tests/src/hashmap.rs', lines 315:0-315:10 -/
def test1 : Result Unit :=
do
let hm ← HashMap.new U64
diff --git a/tests/lean/Hashmap/Types.lean b/tests/lean/Hashmap/Types.lean
index fa454123..c99ba8d0 100644
--- a/tests/lean/Hashmap/Types.lean
+++ b/tests/lean/Hashmap/Types.lean
@@ -6,13 +6,13 @@ open Primitives
namespace hashmap
/- [hashmap::List]
- Source: 'src/hashmap.rs', lines 19:0-19:16 -/
+ Source: 'tests/src/hashmap.rs', lines 19:0-19:16 -/
inductive List (T : Type) :=
| Cons : Usize → T → List T → List T
| Nil : List T
/- [hashmap::HashMap]
- Source: 'src/hashmap.rs', lines 35:0-35:21 -/
+ Source: 'tests/src/hashmap.rs', lines 35:0-35:21 -/
structure HashMap (T : Type) where
num_entries : Usize
max_load_factor : (Usize × Usize)
diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean
index e985ec6a..e27305b1 100644
--- a/tests/lean/HashmapMain/Funs.lean
+++ b/tests/lean/HashmapMain/Funs.lean
@@ -8,12 +8,12 @@ open Primitives
namespace hashmap_main
/- [hashmap_main::hashmap::hash_key]:
- Source: 'src/hashmap.rs', lines 27:0-27:32 -/
+ Source: 'tests/src/hashmap.rs', lines 27:0-27:32 -/
def hashmap.hash_key (k : Usize) : Result Usize :=
Result.ok k
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::allocate_slots]: loop 0:
- Source: 'src/hashmap.rs', lines 50:4-56:5 -/
+ Source: 'tests/src/hashmap.rs', lines 50:4-56:5 -/
divergent def hashmap.HashMap.allocate_slots_loop
(T : Type) (slots : alloc.vec.Vec (hashmap.List T)) (n : Usize) :
Result (alloc.vec.Vec (hashmap.List T))
@@ -27,7 +27,7 @@ divergent def hashmap.HashMap.allocate_slots_loop
else Result.ok slots
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::allocate_slots]:
- Source: 'src/hashmap.rs', lines 50:4-50:76 -/
+ Source: 'tests/src/hashmap.rs', lines 50:4-50:76 -/
def hashmap.HashMap.allocate_slots
(T : Type) (slots : alloc.vec.Vec (hashmap.List T)) (n : Usize) :
Result (alloc.vec.Vec (hashmap.List T))
@@ -35,7 +35,7 @@ def hashmap.HashMap.allocate_slots
hashmap.HashMap.allocate_slots_loop T slots n
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::new_with_capacity]:
- Source: 'src/hashmap.rs', lines 59:4-63:13 -/
+ Source: 'tests/src/hashmap.rs', lines 59:4-63:13 -/
def hashmap.HashMap.new_with_capacity
(T : Type) (capacity : Usize) (max_load_dividend : Usize)
(max_load_divisor : Usize) :
@@ -56,12 +56,12 @@ def hashmap.HashMap.new_with_capacity
}
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::new]:
- Source: 'src/hashmap.rs', lines 75:4-75:24 -/
+ Source: 'tests/src/hashmap.rs', lines 75:4-75:24 -/
def hashmap.HashMap.new (T : Type) : Result (hashmap.HashMap T) :=
hashmap.HashMap.new_with_capacity T 32#usize 4#usize 5#usize
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::clear]: loop 0:
- Source: 'src/hashmap.rs', lines 80:4-88:5 -/
+ Source: 'tests/src/hashmap.rs', lines 80:4-88:5 -/
divergent def hashmap.HashMap.clear_loop
(T : Type) (slots : alloc.vec.Vec (hashmap.List T)) (i : Usize) :
Result (alloc.vec.Vec (hashmap.List T))
@@ -79,7 +79,7 @@ divergent def hashmap.HashMap.clear_loop
else Result.ok slots
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::clear]:
- Source: 'src/hashmap.rs', lines 80:4-80:27 -/
+ Source: 'tests/src/hashmap.rs', lines 80:4-80:27 -/
def hashmap.HashMap.clear
(T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) :=
do
@@ -87,12 +87,12 @@ def hashmap.HashMap.clear
Result.ok { self with num_entries := 0#usize, slots := hm }
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::len]:
- Source: 'src/hashmap.rs', lines 90:4-90:30 -/
+ Source: 'tests/src/hashmap.rs', lines 90:4-90:30 -/
def hashmap.HashMap.len (T : Type) (self : hashmap.HashMap T) : Result Usize :=
Result.ok self.num_entries
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_in_list]: loop 0:
- Source: 'src/hashmap.rs', lines 97:4-114:5 -/
+ Source: 'tests/src/hashmap.rs', lines 97:4-114:5 -/
divergent def hashmap.HashMap.insert_in_list_loop
(T : Type) (key : Usize) (value : T) (ls : hashmap.List T) :
Result (Bool × (hashmap.List T))
@@ -109,7 +109,7 @@ divergent def hashmap.HashMap.insert_in_list_loop
Result.ok (true, hashmap.List.Cons key value hashmap.List.Nil)
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_in_list]:
- Source: 'src/hashmap.rs', lines 97:4-97:71 -/
+ Source: 'tests/src/hashmap.rs', lines 97:4-97:71 -/
def hashmap.HashMap.insert_in_list
(T : Type) (key : Usize) (value : T) (ls : hashmap.List T) :
Result (Bool × (hashmap.List T))
@@ -117,7 +117,7 @@ def hashmap.HashMap.insert_in_list
hashmap.HashMap.insert_in_list_loop T key value ls
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_no_resize]:
- Source: 'src/hashmap.rs', lines 117:4-117:54 -/
+ Source: 'tests/src/hashmap.rs', lines 117:4-117:54 -/
def hashmap.HashMap.insert_no_resize
(T : Type) (self : hashmap.HashMap T) (key : Usize) (value : T) :
Result (hashmap.HashMap T)
@@ -142,7 +142,7 @@ def hashmap.HashMap.insert_no_resize
Result.ok { self with slots := v }
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements_from_list]: loop 0:
- Source: 'src/hashmap.rs', lines 183:4-196:5 -/
+ Source: 'tests/src/hashmap.rs', lines 183:4-196:5 -/
divergent def hashmap.HashMap.move_elements_from_list_loop
(T : Type) (ntable : hashmap.HashMap T) (ls : hashmap.List T) :
Result (hashmap.HashMap T)
@@ -155,7 +155,7 @@ divergent def hashmap.HashMap.move_elements_from_list_loop
| hashmap.List.Nil => Result.ok ntable
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements_from_list]:
- Source: 'src/hashmap.rs', lines 183:4-183:72 -/
+ Source: 'tests/src/hashmap.rs', lines 183:4-183:72 -/
def hashmap.HashMap.move_elements_from_list
(T : Type) (ntable : hashmap.HashMap T) (ls : hashmap.List T) :
Result (hashmap.HashMap T)
@@ -163,7 +163,7 @@ def hashmap.HashMap.move_elements_from_list
hashmap.HashMap.move_elements_from_list_loop T ntable ls
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements]: loop 0:
- Source: 'src/hashmap.rs', lines 171:4-180:5 -/
+ Source: 'tests/src/hashmap.rs', lines 171:4-180:5 -/
divergent def hashmap.HashMap.move_elements_loop
(T : Type) (ntable : hashmap.HashMap T)
(slots : alloc.vec.Vec (hashmap.List T)) (i : Usize) :
@@ -184,7 +184,7 @@ divergent def hashmap.HashMap.move_elements_loop
else Result.ok (ntable, slots)
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements]:
- Source: 'src/hashmap.rs', lines 171:4-171:95 -/
+ Source: 'tests/src/hashmap.rs', lines 171:4-171:95 -/
def hashmap.HashMap.move_elements
(T : Type) (ntable : hashmap.HashMap T)
(slots : alloc.vec.Vec (hashmap.List T)) (i : Usize) :
@@ -193,7 +193,7 @@ def hashmap.HashMap.move_elements
hashmap.HashMap.move_elements_loop T ntable slots i
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::try_resize]:
- Source: 'src/hashmap.rs', lines 140:4-140:28 -/
+ Source: 'tests/src/hashmap.rs', lines 140:4-140:28 -/
def hashmap.HashMap.try_resize
(T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) :=
do
@@ -218,7 +218,7 @@ def hashmap.HashMap.try_resize
else Result.ok { self with max_load_factor := (i, i1) }
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert]:
- Source: 'src/hashmap.rs', lines 129:4-129:48 -/
+ Source: 'tests/src/hashmap.rs', lines 129:4-129:48 -/
def hashmap.HashMap.insert
(T : Type) (self : hashmap.HashMap T) (key : Usize) (value : T) :
Result (hashmap.HashMap T)
@@ -231,7 +231,7 @@ def hashmap.HashMap.insert
else Result.ok self1
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
- Source: 'src/hashmap.rs', lines 206:4-219:5 -/
+ Source: 'tests/src/hashmap.rs', lines 206:4-219:5 -/
divergent def hashmap.HashMap.contains_key_in_list_loop
(T : Type) (key : Usize) (ls : hashmap.List T) : Result Bool :=
match ls with
@@ -242,13 +242,13 @@ divergent def hashmap.HashMap.contains_key_in_list_loop
| hashmap.List.Nil => Result.ok false
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]:
- Source: 'src/hashmap.rs', lines 206:4-206:68 -/
+ Source: 'tests/src/hashmap.rs', lines 206:4-206:68 -/
def hashmap.HashMap.contains_key_in_list
(T : Type) (key : Usize) (ls : hashmap.List T) : Result Bool :=
hashmap.HashMap.contains_key_in_list_loop T key ls
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key]:
- Source: 'src/hashmap.rs', lines 199:4-199:49 -/
+ Source: 'tests/src/hashmap.rs', lines 199:4-199:49 -/
def hashmap.HashMap.contains_key
(T : Type) (self : hashmap.HashMap T) (key : Usize) : Result Bool :=
do
@@ -262,7 +262,7 @@ def hashmap.HashMap.contains_key
hashmap.HashMap.contains_key_in_list T key l
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_in_list]: loop 0:
- Source: 'src/hashmap.rs', lines 224:4-237:5 -/
+ Source: 'tests/src/hashmap.rs', lines 224:4-237:5 -/
divergent def hashmap.HashMap.get_in_list_loop
(T : Type) (key : Usize) (ls : hashmap.List T) : Result T :=
match ls with
@@ -273,13 +273,13 @@ divergent def hashmap.HashMap.get_in_list_loop
| hashmap.List.Nil => Result.fail .panic
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_in_list]:
- Source: 'src/hashmap.rs', lines 224:4-224:70 -/
+ Source: 'tests/src/hashmap.rs', lines 224:4-224:70 -/
def hashmap.HashMap.get_in_list
(T : Type) (key : Usize) (ls : hashmap.List T) : Result T :=
hashmap.HashMap.get_in_list_loop T key ls
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get]:
- Source: 'src/hashmap.rs', lines 239:4-239:55 -/
+ Source: 'tests/src/hashmap.rs', lines 239:4-239:55 -/
def hashmap.HashMap.get
(T : Type) (self : hashmap.HashMap T) (key : Usize) : Result T :=
do
@@ -293,7 +293,7 @@ def hashmap.HashMap.get
hashmap.HashMap.get_in_list T key l
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]: loop 0:
- Source: 'src/hashmap.rs', lines 245:4-254:5 -/
+ Source: 'tests/src/hashmap.rs', lines 245:4-254:5 -/
divergent def hashmap.HashMap.get_mut_in_list_loop
(T : Type) (ls : hashmap.List T) (key : Usize) :
Result (T × (T → Result (hashmap.List T)))
@@ -316,7 +316,7 @@ divergent def hashmap.HashMap.get_mut_in_list_loop
| hashmap.List.Nil => Result.fail .panic
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]:
- Source: 'src/hashmap.rs', lines 245:4-245:86 -/
+ Source: 'tests/src/hashmap.rs', lines 245:4-245:86 -/
def hashmap.HashMap.get_mut_in_list
(T : Type) (ls : hashmap.List T) (key : Usize) :
Result (T × (T → Result (hashmap.List T)))
@@ -324,7 +324,7 @@ def hashmap.HashMap.get_mut_in_list
hashmap.HashMap.get_mut_in_list_loop T ls key
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]:
- Source: 'src/hashmap.rs', lines 257:4-257:67 -/
+ Source: 'tests/src/hashmap.rs', lines 257:4-257:67 -/
def hashmap.HashMap.get_mut
(T : Type) (self : hashmap.HashMap T) (key : Usize) :
Result (T × (T → Result (hashmap.HashMap T)))
@@ -347,7 +347,7 @@ def hashmap.HashMap.get_mut
Result.ok (t, back)
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: loop 0:
- Source: 'src/hashmap.rs', lines 265:4-291:5 -/
+ Source: 'tests/src/hashmap.rs', lines 265:4-291:5 -/
divergent def hashmap.HashMap.remove_from_list_loop
(T : Type) (key : Usize) (ls : hashmap.List T) :
Result ((Option T) × (hashmap.List T))
@@ -369,7 +369,7 @@ divergent def hashmap.HashMap.remove_from_list_loop
| hashmap.List.Nil => Result.ok (none, hashmap.List.Nil)
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]:
- Source: 'src/hashmap.rs', lines 265:4-265:69 -/
+ Source: 'tests/src/hashmap.rs', lines 265:4-265:69 -/
def hashmap.HashMap.remove_from_list
(T : Type) (key : Usize) (ls : hashmap.List T) :
Result ((Option T) × (hashmap.List T))
@@ -377,7 +377,7 @@ def hashmap.HashMap.remove_from_list
hashmap.HashMap.remove_from_list_loop T key ls
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove]:
- Source: 'src/hashmap.rs', lines 294:4-294:52 -/
+ Source: 'tests/src/hashmap.rs', lines 294:4-294:52 -/
def hashmap.HashMap.remove
(T : Type) (self : hashmap.HashMap T) (key : Usize) :
Result ((Option T) × (hashmap.HashMap T))
@@ -403,7 +403,7 @@ def hashmap.HashMap.remove
Result.ok (some x1, { self with num_entries := i1, slots := v })
/- [hashmap_main::hashmap::test1]:
- Source: 'src/hashmap.rs', lines 315:0-315:10 -/
+ Source: 'tests/src/hashmap.rs', lines 315:0-315:10 -/
def hashmap.test1 : Result Unit :=
do
let hm ← hashmap.HashMap.new U64
@@ -447,7 +447,7 @@ def hashmap.test1 : Result Unit :=
else Result.ok ()
/- [hashmap_main::insert_on_disk]:
- Source: 'src/hashmap_main.rs', lines 7:0-7:43 -/
+ Source: 'tests/src/hashmap_main.rs', lines 7:0-7:43 -/
def insert_on_disk
(key : Usize) (value : U64) (st : State) : Result (State × Unit) :=
do
@@ -456,7 +456,7 @@ def insert_on_disk
hashmap_utils.serialize hm1 st1
/- [hashmap_main::main]:
- Source: 'src/hashmap_main.rs', lines 16:0-16:13 -/
+ Source: 'tests/src/hashmap_main.rs', lines 16:0-16:13 -/
def main : Result Unit :=
Result.ok ()
diff --git a/tests/lean/HashmapMain/FunsExternal_Template.lean b/tests/lean/HashmapMain/FunsExternal_Template.lean
index c09edbd2..c9c41608 100644
--- a/tests/lean/HashmapMain/FunsExternal_Template.lean
+++ b/tests/lean/HashmapMain/FunsExternal_Template.lean
@@ -7,12 +7,12 @@ open Primitives
open hashmap_main
/- [hashmap_main::hashmap_utils::deserialize]:
- Source: 'src/hashmap_utils.rs', lines 10:0-10:43 -/
+ Source: 'tests/src/hashmap_utils.rs', lines 10:0-10:43 -/
axiom hashmap_utils.deserialize
: State → Result (State × (hashmap.HashMap U64))
/- [hashmap_main::hashmap_utils::serialize]:
- Source: 'src/hashmap_utils.rs', lines 5:0-5:42 -/
+ Source: 'tests/src/hashmap_utils.rs', lines 5:0-5:42 -/
axiom hashmap_utils.serialize
: hashmap.HashMap U64 → State → Result (State × Unit)
diff --git a/tests/lean/HashmapMain/Types.lean b/tests/lean/HashmapMain/Types.lean
index ae9ac999..076fb9ea 100644
--- a/tests/lean/HashmapMain/Types.lean
+++ b/tests/lean/HashmapMain/Types.lean
@@ -7,13 +7,13 @@ open Primitives
namespace hashmap_main
/- [hashmap_main::hashmap::List]
- Source: 'src/hashmap.rs', lines 19:0-19:16 -/
+ Source: 'tests/src/hashmap.rs', lines 19:0-19:16 -/
inductive hashmap.List (T : Type) :=
| Cons : Usize → T → hashmap.List T → hashmap.List T
| Nil : hashmap.List T
/- [hashmap_main::hashmap::HashMap]
- Source: 'src/hashmap.rs', lines 35:0-35:21 -/
+ Source: 'tests/src/hashmap.rs', lines 35:0-35:21 -/
structure hashmap.HashMap (T : Type) where
num_entries : Usize
max_load_factor : (Usize × Usize)
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index eeba1add..d5bda6ab 100644
--- a/tests/lean/Loops.lean
+++ b/tests/lean/Loops.lean
@@ -6,7 +6,7 @@ open Primitives
namespace loops
/- [loops::sum]: loop 0:
- Source: 'src/loops.rs', lines 4:0-14:1 -/
+ Source: 'tests/src/loops.rs', lines 4:0-14:1 -/
divergent def sum_loop (max : U32) (i : U32) (s : U32) : Result U32 :=
if i < max
then do
@@ -16,12 +16,12 @@ divergent def sum_loop (max : U32) (i : U32) (s : U32) : Result U32 :=
else s * 2#u32
/- [loops::sum]:
- Source: 'src/loops.rs', lines 4:0-4:27 -/
+ Source: 'tests/src/loops.rs', lines 4:0-4:27 -/
def sum (max : U32) : Result U32 :=
sum_loop max 0#u32 0#u32
/- [loops::sum_with_mut_borrows]: loop 0:
- Source: 'src/loops.rs', lines 19:0-31:1 -/
+ Source: 'tests/src/loops.rs', lines 19:0-31:1 -/
divergent def sum_with_mut_borrows_loop
(max : U32) (i : U32) (s : U32) : Result U32 :=
if i < max
@@ -33,12 +33,12 @@ divergent def sum_with_mut_borrows_loop
else s * 2#u32
/- [loops::sum_with_mut_borrows]:
- Source: 'src/loops.rs', lines 19:0-19:44 -/
+ Source: 'tests/src/loops.rs', lines 19:0-19:44 -/
def sum_with_mut_borrows (max : U32) : Result U32 :=
sum_with_mut_borrows_loop max 0#u32 0#u32
/- [loops::sum_with_shared_borrows]: loop 0:
- Source: 'src/loops.rs', lines 34:0-48:1 -/
+ Source: 'tests/src/loops.rs', lines 34:0-48:1 -/
divergent def sum_with_shared_borrows_loop
(max : U32) (i : U32) (s : U32) : Result U32 :=
if i < max
@@ -50,12 +50,12 @@ divergent def sum_with_shared_borrows_loop
else s * 2#u32
/- [loops::sum_with_shared_borrows]:
- Source: 'src/loops.rs', lines 34:0-34:47 -/
+ Source: 'tests/src/loops.rs', lines 34:0-34:47 -/
def sum_with_shared_borrows (max : U32) : Result U32 :=
sum_with_shared_borrows_loop max 0#u32 0#u32
/- [loops::sum_array]: loop 0:
- Source: 'src/loops.rs', lines 50:0-58:1 -/
+ Source: 'tests/src/loops.rs', lines 50:0-58:1 -/
divergent def sum_array_loop
(N : Usize) (a : Array U32 N) (i : Usize) (s : U32) : Result U32 :=
if i < N
@@ -68,12 +68,12 @@ divergent def sum_array_loop
else Result.ok s
/- [loops::sum_array]:
- Source: 'src/loops.rs', lines 50:0-50:52 -/
+ Source: 'tests/src/loops.rs', lines 50:0-50:52 -/
def sum_array (N : Usize) (a : Array U32 N) : Result U32 :=
sum_array_loop N a 0#usize 0#u32
/- [loops::clear]: loop 0:
- Source: 'src/loops.rs', lines 62:0-68:1 -/
+ Source: 'tests/src/loops.rs', lines 62:0-68:1 -/
divergent def clear_loop
(v : alloc.vec.Vec U32) (i : Usize) : Result (alloc.vec.Vec U32) :=
let i1 := alloc.vec.Vec.len U32 v
@@ -89,18 +89,18 @@ divergent def clear_loop
else Result.ok v
/- [loops::clear]:
- Source: 'src/loops.rs', lines 62:0-62:30 -/
+ Source: 'tests/src/loops.rs', lines 62:0-62:30 -/
def clear (v : alloc.vec.Vec U32) : Result (alloc.vec.Vec U32) :=
clear_loop v 0#usize
/- [loops::List]
- Source: 'src/loops.rs', lines 70:0-70:16 -/
+ Source: 'tests/src/loops.rs', lines 70:0-70:16 -/
inductive List (T : Type) :=
| Cons : T → List T → List T
| Nil : List T
/- [loops::list_mem]: loop 0:
- Source: 'src/loops.rs', lines 76:0-85:1 -/
+ Source: 'tests/src/loops.rs', lines 76:0-85:1 -/
divergent def list_mem_loop (x : U32) (ls : List U32) : Result Bool :=
match ls with
| List.Cons y tl => if y = x
@@ -109,12 +109,12 @@ divergent def list_mem_loop (x : U32) (ls : List U32) : Result Bool :=
| List.Nil => Result.ok false
/- [loops::list_mem]:
- Source: 'src/loops.rs', lines 76:0-76:52 -/
+ Source: 'tests/src/loops.rs', lines 76:0-76:52 -/
def list_mem (x : U32) (ls : List U32) : Result Bool :=
list_mem_loop x ls
/- [loops::list_nth_mut_loop]: loop 0:
- Source: 'src/loops.rs', lines 88:0-98:1 -/
+ Source: 'tests/src/loops.rs', lines 88:0-98:1 -/
divergent def list_nth_mut_loop_loop
(T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) :=
match ls with
@@ -135,13 +135,13 @@ divergent def list_nth_mut_loop_loop
| List.Nil => Result.fail .panic
/- [loops::list_nth_mut_loop]:
- Source: 'src/loops.rs', lines 88:0-88:71 -/
+ Source: 'tests/src/loops.rs', lines 88:0-88:71 -/
def list_nth_mut_loop
(T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) :=
list_nth_mut_loop_loop T ls i
/- [loops::list_nth_shared_loop]: loop 0:
- Source: 'src/loops.rs', lines 101:0-111:1 -/
+ Source: 'tests/src/loops.rs', lines 101:0-111:1 -/
divergent def list_nth_shared_loop_loop
(T : Type) (ls : List T) (i : U32) : Result T :=
match ls with
@@ -154,12 +154,12 @@ divergent def list_nth_shared_loop_loop
| List.Nil => Result.fail .panic
/- [loops::list_nth_shared_loop]:
- Source: 'src/loops.rs', lines 101:0-101:66 -/
+ Source: 'tests/src/loops.rs', lines 101:0-101:66 -/
def list_nth_shared_loop (T : Type) (ls : List T) (i : U32) : Result T :=
list_nth_shared_loop_loop T ls i
/- [loops::get_elem_mut]: loop 0:
- Source: 'src/loops.rs', lines 113:0-127:1 -/
+ Source: 'tests/src/loops.rs', lines 113:0-127:1 -/
divergent def get_elem_mut_loop
(x : Usize) (ls : List Usize) :
Result (Usize × (Usize → Result (List Usize)))
@@ -181,7 +181,7 @@ divergent def get_elem_mut_loop
| List.Nil => Result.fail .panic
/- [loops::get_elem_mut]:
- Source: 'src/loops.rs', lines 113:0-113:73 -/
+ Source: 'tests/src/loops.rs', lines 113:0-113:73 -/
def get_elem_mut
(slots : alloc.vec.Vec (List Usize)) (x : Usize) :
Result (Usize × (Usize → Result (alloc.vec.Vec (List Usize))))
@@ -197,7 +197,7 @@ def get_elem_mut
Result.ok (i, back1)
/- [loops::get_elem_shared]: loop 0:
- Source: 'src/loops.rs', lines 129:0-143:1 -/
+ Source: 'tests/src/loops.rs', lines 129:0-143:1 -/
divergent def get_elem_shared_loop
(x : Usize) (ls : List Usize) : Result Usize :=
match ls with
@@ -207,7 +207,7 @@ divergent def get_elem_shared_loop
| List.Nil => Result.fail .panic
/- [loops::get_elem_shared]:
- Source: 'src/loops.rs', lines 129:0-129:68 -/
+ Source: 'tests/src/loops.rs', lines 129:0-129:68 -/
def get_elem_shared
(slots : alloc.vec.Vec (List Usize)) (x : Usize) : Result Usize :=
do
@@ -217,7 +217,7 @@ def get_elem_shared
get_elem_shared_loop x ls
/- [loops::id_mut]:
- Source: 'src/loops.rs', lines 145:0-145:50 -/
+ Source: 'tests/src/loops.rs', lines 145:0-145:50 -/
def id_mut
(T : Type) (ls : List T) :
Result ((List T) × (List T → Result (List T)))
@@ -225,12 +225,12 @@ def id_mut
Result.ok (ls, Result.ok)
/- [loops::id_shared]:
- Source: 'src/loops.rs', lines 149:0-149:45 -/
+ Source: 'tests/src/loops.rs', lines 149:0-149:45 -/
def id_shared (T : Type) (ls : List T) : Result (List T) :=
Result.ok ls
/- [loops::list_nth_mut_loop_with_id]: loop 0:
- Source: 'src/loops.rs', lines 154:0-165:1 -/
+ Source: 'tests/src/loops.rs', lines 154:0-165:1 -/
divergent def list_nth_mut_loop_with_id_loop
(T : Type) (i : U32) (ls : List T) : Result (T × (T → Result (List T))) :=
match ls with
@@ -251,7 +251,7 @@ divergent def list_nth_mut_loop_with_id_loop
| List.Nil => Result.fail .panic
/- [loops::list_nth_mut_loop_with_id]:
- Source: 'src/loops.rs', lines 154:0-154:75 -/
+ Source: 'tests/src/loops.rs', lines 154:0-154:75 -/
def list_nth_mut_loop_with_id
(T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) :=
do
@@ -263,7 +263,7 @@ def list_nth_mut_loop_with_id
Result.ok (t, back1)
/- [loops::list_nth_shared_loop_with_id]: loop 0:
- Source: 'src/loops.rs', lines 168:0-179:1 -/
+ Source: 'tests/src/loops.rs', lines 168:0-179:1 -/
divergent def list_nth_shared_loop_with_id_loop
(T : Type) (i : U32) (ls : List T) : Result T :=
match ls with
@@ -276,7 +276,7 @@ divergent def list_nth_shared_loop_with_id_loop
| List.Nil => Result.fail .panic
/- [loops::list_nth_shared_loop_with_id]:
- Source: 'src/loops.rs', lines 168:0-168:70 -/
+ Source: 'tests/src/loops.rs', lines 168:0-168:70 -/
def list_nth_shared_loop_with_id
(T : Type) (ls : List T) (i : U32) : Result T :=
do
@@ -284,7 +284,7 @@ def list_nth_shared_loop_with_id
list_nth_shared_loop_with_id_loop T i ls1
/- [loops::list_nth_mut_loop_pair]: loop 0:
- Source: 'src/loops.rs', lines 184:0-205:1 -/
+ Source: 'tests/src/loops.rs', lines 184:0-205:1 -/
divergent def list_nth_mut_loop_pair_loop
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × (T → Result (List T)) × (T → Result (List T)))
@@ -315,7 +315,7 @@ divergent def list_nth_mut_loop_pair_loop
| List.Nil => Result.fail .panic
/- [loops::list_nth_mut_loop_pair]:
- Source: 'src/loops.rs', lines 184:0-188:27 -/
+ Source: 'tests/src/loops.rs', lines 184:0-188:27 -/
def list_nth_mut_loop_pair
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × (T → Result (List T)) × (T → Result (List T)))
@@ -323,7 +323,7 @@ def list_nth_mut_loop_pair
list_nth_mut_loop_pair_loop T ls0 ls1 i
/- [loops::list_nth_shared_loop_pair]: loop 0:
- Source: 'src/loops.rs', lines 208:0-229:1 -/
+ Source: 'tests/src/loops.rs', lines 208:0-229:1 -/
divergent def list_nth_shared_loop_pair_loop
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
match ls0 with
@@ -339,13 +339,13 @@ divergent def list_nth_shared_loop_pair_loop
| List.Nil => Result.fail .panic
/- [loops::list_nth_shared_loop_pair]:
- Source: 'src/loops.rs', lines 208:0-212:19 -/
+ Source: 'tests/src/loops.rs', lines 208:0-212:19 -/
def list_nth_shared_loop_pair
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
list_nth_shared_loop_pair_loop T ls0 ls1 i
/- [loops::list_nth_mut_loop_pair_merge]: loop 0:
- Source: 'src/loops.rs', lines 233:0-248:1 -/
+ Source: 'tests/src/loops.rs', lines 233:0-248:1 -/
divergent def list_nth_mut_loop_pair_merge_loop
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × ((T × T) → Result ((List T) × (List T))))
@@ -375,7 +375,7 @@ divergent def list_nth_mut_loop_pair_merge_loop
| List.Nil => Result.fail .panic
/- [loops::list_nth_mut_loop_pair_merge]:
- Source: 'src/loops.rs', lines 233:0-237:27 -/
+ Source: 'tests/src/loops.rs', lines 233:0-237:27 -/
def list_nth_mut_loop_pair_merge
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × ((T × T) → Result ((List T) × (List T))))
@@ -383,7 +383,7 @@ def list_nth_mut_loop_pair_merge
list_nth_mut_loop_pair_merge_loop T ls0 ls1 i
/- [loops::list_nth_shared_loop_pair_merge]: loop 0:
- Source: 'src/loops.rs', lines 251:0-266:1 -/
+ Source: 'tests/src/loops.rs', lines 251:0-266:1 -/
divergent def list_nth_shared_loop_pair_merge_loop
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
match ls0 with
@@ -400,13 +400,13 @@ divergent def list_nth_shared_loop_pair_merge_loop
| List.Nil => Result.fail .panic
/- [loops::list_nth_shared_loop_pair_merge]:
- Source: 'src/loops.rs', lines 251:0-255:19 -/
+ Source: 'tests/src/loops.rs', lines 251:0-255:19 -/
def list_nth_shared_loop_pair_merge
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
list_nth_shared_loop_pair_merge_loop T ls0 ls1 i
/- [loops::list_nth_mut_shared_loop_pair]: loop 0:
- Source: 'src/loops.rs', lines 269:0-284:1 -/
+ Source: 'tests/src/loops.rs', lines 269:0-284:1 -/
divergent def list_nth_mut_shared_loop_pair_loop
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × (T → Result (List T)))
@@ -432,7 +432,7 @@ divergent def list_nth_mut_shared_loop_pair_loop
| List.Nil => Result.fail .panic
/- [loops::list_nth_mut_shared_loop_pair]:
- Source: 'src/loops.rs', lines 269:0-273:23 -/
+ Source: 'tests/src/loops.rs', lines 269:0-273:23 -/
def list_nth_mut_shared_loop_pair
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × (T → Result (List T)))
@@ -440,7 +440,7 @@ def list_nth_mut_shared_loop_pair
list_nth_mut_shared_loop_pair_loop T ls0 ls1 i
/- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0:
- Source: 'src/loops.rs', lines 288:0-303:1 -/
+ Source: 'tests/src/loops.rs', lines 288:0-303:1 -/
divergent def list_nth_mut_shared_loop_pair_merge_loop
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × (T → Result (List T)))
@@ -466,7 +466,7 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop
| List.Nil => Result.fail .panic
/- [loops::list_nth_mut_shared_loop_pair_merge]:
- Source: 'src/loops.rs', lines 288:0-292:23 -/
+ Source: 'tests/src/loops.rs', lines 288:0-292:23 -/
def list_nth_mut_shared_loop_pair_merge
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × (T → Result (List T)))
@@ -474,7 +474,7 @@ def list_nth_mut_shared_loop_pair_merge
list_nth_mut_shared_loop_pair_merge_loop T ls0 ls1 i
/- [loops::list_nth_shared_mut_loop_pair]: loop 0:
- Source: 'src/loops.rs', lines 307:0-322:1 -/
+ Source: 'tests/src/loops.rs', lines 307:0-322:1 -/
divergent def list_nth_shared_mut_loop_pair_loop
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × (T → Result (List T)))
@@ -500,7 +500,7 @@ divergent def list_nth_shared_mut_loop_pair_loop
| List.Nil => Result.fail .panic
/- [loops::list_nth_shared_mut_loop_pair]:
- Source: 'src/loops.rs', lines 307:0-311:23 -/
+ Source: 'tests/src/loops.rs', lines 307:0-311:23 -/
def list_nth_shared_mut_loop_pair
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × (T → Result (List T)))
@@ -508,7 +508,7 @@ def list_nth_shared_mut_loop_pair
list_nth_shared_mut_loop_pair_loop T ls0 ls1 i
/- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0:
- Source: 'src/loops.rs', lines 326:0-341:1 -/
+ Source: 'tests/src/loops.rs', lines 326:0-341:1 -/
divergent def list_nth_shared_mut_loop_pair_merge_loop
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × (T → Result (List T)))
@@ -534,7 +534,7 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop
| List.Nil => Result.fail .panic
/- [loops::list_nth_shared_mut_loop_pair_merge]:
- Source: 'src/loops.rs', lines 326:0-330:23 -/
+ Source: 'tests/src/loops.rs', lines 326:0-330:23 -/
def list_nth_shared_mut_loop_pair_merge
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × (T → Result (List T)))
@@ -542,7 +542,7 @@ def list_nth_shared_mut_loop_pair_merge
list_nth_shared_mut_loop_pair_merge_loop T ls0 ls1 i
/- [loops::ignore_input_mut_borrow]: loop 0:
- Source: 'src/loops.rs', lines 345:0-349:1 -/
+ Source: 'tests/src/loops.rs', lines 345:0-349:1 -/
divergent def ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
if i > 0#u32
then do
@@ -551,14 +551,14 @@ divergent def ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
else Result.ok ()
/- [loops::ignore_input_mut_borrow]:
- Source: 'src/loops.rs', lines 345:0-345:56 -/
+ Source: 'tests/src/loops.rs', lines 345:0-345:56 -/
def ignore_input_mut_borrow (_a : U32) (i : U32) : Result U32 :=
do
let _ ← ignore_input_mut_borrow_loop i
Result.ok _a
/- [loops::incr_ignore_input_mut_borrow]: loop 0:
- Source: 'src/loops.rs', lines 353:0-358:1 -/
+ Source: 'tests/src/loops.rs', lines 353:0-358:1 -/
divergent def incr_ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
if i > 0#u32
then do
@@ -567,7 +567,7 @@ divergent def incr_ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
else Result.ok ()
/- [loops::incr_ignore_input_mut_borrow]:
- Source: 'src/loops.rs', lines 353:0-353:60 -/
+ Source: 'tests/src/loops.rs', lines 353:0-353:60 -/
def incr_ignore_input_mut_borrow (a : U32) (i : U32) : Result U32 :=
do
let a1 ← a + 1#u32
@@ -575,7 +575,7 @@ def incr_ignore_input_mut_borrow (a : U32) (i : U32) : Result U32 :=
Result.ok a1
/- [loops::ignore_input_shared_borrow]: loop 0:
- Source: 'src/loops.rs', lines 362:0-366:1 -/
+ Source: 'tests/src/loops.rs', lines 362:0-366:1 -/
divergent def ignore_input_shared_borrow_loop (i : U32) : Result Unit :=
if i > 0#u32
then do
@@ -584,7 +584,7 @@ divergent def ignore_input_shared_borrow_loop (i : U32) : Result Unit :=
else Result.ok ()
/- [loops::ignore_input_shared_borrow]:
- Source: 'src/loops.rs', lines 362:0-362:59 -/
+ Source: 'tests/src/loops.rs', lines 362:0-362:59 -/
def ignore_input_shared_borrow (_a : U32) (i : U32) : Result U32 :=
do
let _ ← ignore_input_shared_borrow_loop i
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 66ec917b..5ae22055 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -6,60 +6,60 @@ open Primitives
namespace no_nested_borrows
/- [no_nested_borrows::Pair]
- Source: 'src/no_nested_borrows.rs', lines 4:0-4:23 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 4:0-4:23 -/
structure Pair (T1 T2 : Type) where
x : T1
y : T2
/- [no_nested_borrows::List]
- Source: 'src/no_nested_borrows.rs', lines 9:0-9:16 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 9:0-9:16 -/
inductive List (T : Type) :=
| Cons : T → List T → List T
| Nil : List T
/- [no_nested_borrows::One]
- Source: 'src/no_nested_borrows.rs', lines 20:0-20:16 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 20:0-20:16 -/
inductive One (T1 : Type) :=
| One : T1 → One T1
/- [no_nested_borrows::EmptyEnum]
- Source: 'src/no_nested_borrows.rs', lines 26:0-26:18 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 26:0-26:18 -/
inductive EmptyEnum :=
| Empty : EmptyEnum
/- [no_nested_borrows::Enum]
- Source: 'src/no_nested_borrows.rs', lines 32:0-32:13 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 32:0-32:13 -/
inductive Enum :=
| Variant1 : Enum
| Variant2 : Enum
/- [no_nested_borrows::EmptyStruct]
- Source: 'src/no_nested_borrows.rs', lines 39:0-39:22 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 39:0-39:22 -/
@[reducible] def EmptyStruct := Unit
/- [no_nested_borrows::Sum]
- Source: 'src/no_nested_borrows.rs', lines 41:0-41:20 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 41:0-41:20 -/
inductive Sum (T1 T2 : Type) :=
| Left : T1 → Sum T1 T2
| Right : T2 → Sum T1 T2
/- [no_nested_borrows::cast_u32_to_i32]:
- Source: 'src/no_nested_borrows.rs', lines 46:0-46:37 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 46:0-46:37 -/
def cast_u32_to_i32 (x : U32) : Result I32 :=
Scalar.cast .I32 x
/- [no_nested_borrows::cast_bool_to_i32]:
- Source: 'src/no_nested_borrows.rs', lines 50:0-50:39 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 50:0-50:39 -/
def cast_bool_to_i32 (x : Bool) : Result I32 :=
Scalar.cast_bool .I32 x
/- [no_nested_borrows::cast_bool_to_bool]:
- Source: 'src/no_nested_borrows.rs', lines 55:0-55:41 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 55:0-55:41 -/
def cast_bool_to_bool (x : Bool) : Result Bool :=
Result.ok x
/- [no_nested_borrows::test2]:
- Source: 'src/no_nested_borrows.rs', lines 60:0-60:14 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 60:0-60:14 -/
def test2 : Result Unit :=
do
let _ ← 23#u32 + 44#u32
@@ -69,14 +69,14 @@ def test2 : Result Unit :=
#assert (test2 == Result.ok ())
/- [no_nested_borrows::get_max]:
- Source: 'src/no_nested_borrows.rs', lines 72:0-72:37 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 72:0-72:37 -/
def get_max (x : U32) (y : U32) : Result U32 :=
if x >= y
then Result.ok x
else Result.ok y
/- [no_nested_borrows::test3]:
- Source: 'src/no_nested_borrows.rs', lines 80:0-80:14 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 80:0-80:14 -/
def test3 : Result Unit :=
do
let x ← get_max 4#u32 3#u32
@@ -90,7 +90,7 @@ def test3 : Result Unit :=
#assert (test3 == Result.ok ())
/- [no_nested_borrows::test_neg1]:
- Source: 'src/no_nested_borrows.rs', lines 87:0-87:18 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 87:0-87:18 -/
def test_neg1 : Result Unit :=
do
let y ← -. 3#i32
@@ -102,7 +102,7 @@ def test_neg1 : Result Unit :=
#assert (test_neg1 == Result.ok ())
/- [no_nested_borrows::refs_test1]:
- Source: 'src/no_nested_borrows.rs', lines 94:0-94:19 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 94:0-94:19 -/
def refs_test1 : Result Unit :=
if ¬ (1#i32 = 1#i32)
then Result.fail .panic
@@ -112,7 +112,7 @@ def refs_test1 : Result Unit :=
#assert (refs_test1 == Result.ok ())
/- [no_nested_borrows::refs_test2]:
- Source: 'src/no_nested_borrows.rs', lines 105:0-105:19 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 105:0-105:19 -/
def refs_test2 : Result Unit :=
if ¬ (2#i32 = 2#i32)
then Result.fail .panic
@@ -130,7 +130,7 @@ def refs_test2 : Result Unit :=
#assert (refs_test2 == Result.ok ())
/- [no_nested_borrows::test_list1]:
- Source: 'src/no_nested_borrows.rs', lines 121:0-121:19 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 121:0-121:19 -/
def test_list1 : Result Unit :=
Result.ok ()
@@ -138,7 +138,7 @@ def test_list1 : Result Unit :=
#assert (test_list1 == Result.ok ())
/- [no_nested_borrows::test_box1]:
- Source: 'src/no_nested_borrows.rs', lines 126:0-126:18 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 126:0-126:18 -/
def test_box1 : Result Unit :=
do
let (_, deref_mut_back) ← alloc.boxed.Box.deref_mut I32 0#i32
@@ -152,26 +152,26 @@ def test_box1 : Result Unit :=
#assert (test_box1 == Result.ok ())
/- [no_nested_borrows::copy_int]:
- Source: 'src/no_nested_borrows.rs', lines 136:0-136:30 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 136:0-136:30 -/
def copy_int (x : I32) : Result I32 :=
Result.ok x
/- [no_nested_borrows::test_unreachable]:
- Source: 'src/no_nested_borrows.rs', lines 142:0-142:32 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 142:0-142:32 -/
def test_unreachable (b : Bool) : Result Unit :=
if b
then Result.fail .panic
else Result.ok ()
/- [no_nested_borrows::test_panic]:
- Source: 'src/no_nested_borrows.rs', lines 150:0-150:26 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 150:0-150:26 -/
def test_panic (b : Bool) : Result Unit :=
if b
then Result.fail .panic
else Result.ok ()
/- [no_nested_borrows::test_copy_int]:
- Source: 'src/no_nested_borrows.rs', lines 157:0-157:22 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 157:0-157:22 -/
def test_copy_int : Result Unit :=
do
let y ← copy_int 0#i32
@@ -183,14 +183,14 @@ def test_copy_int : Result Unit :=
#assert (test_copy_int == Result.ok ())
/- [no_nested_borrows::is_cons]:
- Source: 'src/no_nested_borrows.rs', lines 164:0-164:38 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 164:0-164:38 -/
def is_cons (T : Type) (l : List T) : Result Bool :=
match l with
| List.Cons _ _ => Result.ok true
| List.Nil => Result.ok false
/- [no_nested_borrows::test_is_cons]:
- Source: 'src/no_nested_borrows.rs', lines 171:0-171:21 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 171:0-171:21 -/
def test_is_cons : Result Unit :=
do
let b ← is_cons I32 (List.Cons 0#i32 List.Nil)
@@ -202,14 +202,14 @@ def test_is_cons : Result Unit :=
#assert (test_is_cons == Result.ok ())
/- [no_nested_borrows::split_list]:
- Source: 'src/no_nested_borrows.rs', lines 177:0-177:48 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 177:0-177:48 -/
def split_list (T : Type) (l : List T) : Result (T × (List T)) :=
match l with
| List.Cons hd tl => Result.ok (hd, tl)
| List.Nil => Result.fail .panic
/- [no_nested_borrows::test_split_list]:
- Source: 'src/no_nested_borrows.rs', lines 185:0-185:24 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 185:0-185:24 -/
def test_split_list : Result Unit :=
do
let p ← split_list I32 (List.Cons 0#i32 List.Nil)
@@ -222,7 +222,7 @@ def test_split_list : Result Unit :=
#assert (test_split_list == Result.ok ())
/- [no_nested_borrows::choose]:
- Source: 'src/no_nested_borrows.rs', lines 192:0-192:70 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 192:0-192:70 -/
def choose
(T : Type) (b : Bool) (x : T) (y : T) :
Result (T × (T → Result (T × T)))
@@ -234,7 +234,7 @@ def choose
Result.ok (y, back)
/- [no_nested_borrows::choose_test]:
- Source: 'src/no_nested_borrows.rs', lines 200:0-200:20 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 200:0-200:20 -/
def choose_test : Result Unit :=
do
let (z, choose_back) ← choose I32 true 0#i32 0#i32
@@ -254,20 +254,20 @@ def choose_test : Result Unit :=
#assert (choose_test == Result.ok ())
/- [no_nested_borrows::test_char]:
- Source: 'src/no_nested_borrows.rs', lines 212:0-212:26 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 212:0-212:26 -/
def test_char : Result Char :=
Result.ok 'a'
mutual
/- [no_nested_borrows::Tree]
- Source: 'src/no_nested_borrows.rs', lines 217:0-217:16 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 217:0-217:16 -/
inductive Tree (T : Type) :=
| Leaf : T → Tree T
| Node : T → NodeElem T → Tree T → Tree T
/- [no_nested_borrows::NodeElem]
- Source: 'src/no_nested_borrows.rs', lines 222:0-222:20 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 222:0-222:20 -/
inductive NodeElem (T : Type) :=
| Cons : Tree T → NodeElem T → NodeElem T
| Nil : NodeElem T
@@ -275,7 +275,7 @@ inductive NodeElem (T : Type) :=
end
/- [no_nested_borrows::list_length]:
- Source: 'src/no_nested_borrows.rs', lines 257:0-257:48 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 257:0-257:48 -/
divergent def list_length (T : Type) (l : List T) : Result U32 :=
match l with
| List.Cons _ l1 => do
@@ -284,7 +284,7 @@ divergent def list_length (T : Type) (l : List T) : Result U32 :=
| List.Nil => Result.ok 0#u32
/- [no_nested_borrows::list_nth_shared]:
- Source: 'src/no_nested_borrows.rs', lines 265:0-265:62 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 265:0-265:62 -/
divergent def list_nth_shared (T : Type) (l : List T) (i : U32) : Result T :=
match l with
| List.Cons x tl =>
@@ -296,7 +296,7 @@ divergent def list_nth_shared (T : Type) (l : List T) (i : U32) : Result T :=
| List.Nil => Result.fail .panic
/- [no_nested_borrows::list_nth_mut]:
- Source: 'src/no_nested_borrows.rs', lines 281:0-281:67 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 281:0-281:67 -/
divergent def list_nth_mut
(T : Type) (l : List T) (i : U32) : Result (T × (T → Result (List T))) :=
match l with
@@ -318,7 +318,7 @@ divergent def list_nth_mut
| List.Nil => Result.fail .panic
/- [no_nested_borrows::list_rev_aux]:
- Source: 'src/no_nested_borrows.rs', lines 297:0-297:63 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 297:0-297:63 -/
divergent def list_rev_aux
(T : Type) (li : List T) (lo : List T) : Result (List T) :=
match li with
@@ -326,13 +326,13 @@ divergent def list_rev_aux
| List.Nil => Result.ok lo
/- [no_nested_borrows::list_rev]:
- Source: 'src/no_nested_borrows.rs', lines 311:0-311:42 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 311:0-311:42 -/
def list_rev (T : Type) (l : List T) : Result (List T) :=
let (li, _) := core.mem.replace (List T) l List.Nil
list_rev_aux T li List.Nil
/- [no_nested_borrows::test_list_functions]:
- Source: 'src/no_nested_borrows.rs', lines 316:0-316:28 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 316:0-316:28 -/
def test_list_functions : Result Unit :=
do
let l := List.Cons 2#i32 List.Nil
@@ -379,7 +379,7 @@ def test_list_functions : Result Unit :=
#assert (test_list_functions == Result.ok ())
/- [no_nested_borrows::id_mut_pair1]:
- Source: 'src/no_nested_borrows.rs', lines 332:0-332:89 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 332:0-332:89 -/
def id_mut_pair1
(T1 T2 : Type) (x : T1) (y : T2) :
Result ((T1 × T2) × ((T1 × T2) → Result (T1 × T2)))
@@ -387,7 +387,7 @@ def id_mut_pair1
Result.ok ((x, y), Result.ok)
/- [no_nested_borrows::id_mut_pair2]:
- Source: 'src/no_nested_borrows.rs', lines 336:0-336:88 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 336:0-336:88 -/
def id_mut_pair2
(T1 T2 : Type) (p : (T1 × T2)) :
Result ((T1 × T2) × ((T1 × T2) → Result (T1 × T2)))
@@ -396,7 +396,7 @@ def id_mut_pair2
Result.ok ((t, t1), Result.ok)
/- [no_nested_borrows::id_mut_pair3]:
- Source: 'src/no_nested_borrows.rs', lines 340:0-340:93 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 340:0-340:93 -/
def id_mut_pair3
(T1 T2 : Type) (x : T1) (y : T2) :
Result ((T1 × T2) × (T1 → Result T1) × (T2 → Result T2))
@@ -404,7 +404,7 @@ def id_mut_pair3
Result.ok ((x, y), Result.ok, Result.ok)
/- [no_nested_borrows::id_mut_pair4]:
- Source: 'src/no_nested_borrows.rs', lines 344:0-344:92 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 344:0-344:92 -/
def id_mut_pair4
(T1 T2 : Type) (p : (T1 × T2)) :
Result ((T1 × T2) × (T1 → Result T1) × (T2 → Result T2))
@@ -413,37 +413,37 @@ def id_mut_pair4
Result.ok ((t, t1), Result.ok, Result.ok)
/- [no_nested_borrows::StructWithTuple]
- Source: 'src/no_nested_borrows.rs', lines 351:0-351:34 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 351:0-351:34 -/
structure StructWithTuple (T1 T2 : Type) where
p : (T1 × T2)
/- [no_nested_borrows::new_tuple1]:
- Source: 'src/no_nested_borrows.rs', lines 355:0-355:48 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 355:0-355:48 -/
def new_tuple1 : Result (StructWithTuple U32 U32) :=
Result.ok { p := (1#u32, 2#u32) }
/- [no_nested_borrows::new_tuple2]:
- Source: 'src/no_nested_borrows.rs', lines 359:0-359:48 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 359:0-359:48 -/
def new_tuple2 : Result (StructWithTuple I16 I16) :=
Result.ok { p := (1#i16, 2#i16) }
/- [no_nested_borrows::new_tuple3]:
- Source: 'src/no_nested_borrows.rs', lines 363:0-363:48 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 363:0-363:48 -/
def new_tuple3 : Result (StructWithTuple U64 I64) :=
Result.ok { p := (1#u64, 2#i64) }
/- [no_nested_borrows::StructWithPair]
- Source: 'src/no_nested_borrows.rs', lines 368:0-368:33 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 368:0-368:33 -/
structure StructWithPair (T1 T2 : Type) where
p : Pair T1 T2
/- [no_nested_borrows::new_pair1]:
- Source: 'src/no_nested_borrows.rs', lines 372:0-372:46 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 372:0-372:46 -/
def new_pair1 : Result (StructWithPair U32 U32) :=
Result.ok { p := { x := 1#u32, y := 2#u32 } }
/- [no_nested_borrows::test_constants]:
- Source: 'src/no_nested_borrows.rs', lines 380:0-380:23 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 380:0-380:23 -/
def test_constants : Result Unit :=
do
let swt ← new_tuple1
@@ -473,7 +473,7 @@ def test_constants : Result Unit :=
#assert (test_constants == Result.ok ())
/- [no_nested_borrows::test_weird_borrows1]:
- Source: 'src/no_nested_borrows.rs', lines 389:0-389:28 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 389:0-389:28 -/
def test_weird_borrows1 : Result Unit :=
Result.ok ()
@@ -481,7 +481,7 @@ def test_weird_borrows1 : Result Unit :=
#assert (test_weird_borrows1 == Result.ok ())
/- [no_nested_borrows::test_mem_replace]:
- Source: 'src/no_nested_borrows.rs', lines 399:0-399:37 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 399:0-399:37 -/
def test_mem_replace (px : U32) : Result U32 :=
let (y, _) := core.mem.replace U32 px 1#u32
if ¬ (y = 0#u32)
@@ -489,71 +489,71 @@ def test_mem_replace (px : U32) : Result U32 :=
else Result.ok 2#u32
/- [no_nested_borrows::test_shared_borrow_bool1]:
- Source: 'src/no_nested_borrows.rs', lines 406:0-406:47 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 406:0-406:47 -/
def test_shared_borrow_bool1 (b : Bool) : Result U32 :=
if b
then Result.ok 0#u32
else Result.ok 1#u32
/- [no_nested_borrows::test_shared_borrow_bool2]:
- Source: 'src/no_nested_borrows.rs', lines 419:0-419:40 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 419:0-419:40 -/
def test_shared_borrow_bool2 : Result U32 :=
Result.ok 0#u32
/- [no_nested_borrows::test_shared_borrow_enum1]:
- Source: 'src/no_nested_borrows.rs', lines 434:0-434:52 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 434:0-434:52 -/
def test_shared_borrow_enum1 (l : List U32) : Result U32 :=
match l with
| List.Cons _ _ => Result.ok 1#u32
| List.Nil => Result.ok 0#u32
/- [no_nested_borrows::test_shared_borrow_enum2]:
- Source: 'src/no_nested_borrows.rs', lines 446:0-446:40 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 446:0-446:40 -/
def test_shared_borrow_enum2 : Result U32 :=
Result.ok 0#u32
/- [no_nested_borrows::incr]:
- Source: 'src/no_nested_borrows.rs', lines 457:0-457:24 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 457:0-457:24 -/
def incr (x : U32) : Result U32 :=
x + 1#u32
/- [no_nested_borrows::call_incr]:
- Source: 'src/no_nested_borrows.rs', lines 461:0-461:35 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 461:0-461:35 -/
def call_incr (x : U32) : Result U32 :=
incr x
/- [no_nested_borrows::read_then_incr]:
- Source: 'src/no_nested_borrows.rs', lines 466:0-466:41 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 466:0-466:41 -/
def read_then_incr (x : U32) : Result (U32 × U32) :=
do
let x1 ← x + 1#u32
Result.ok (x, x1)
/- [no_nested_borrows::Tuple]
- Source: 'src/no_nested_borrows.rs', lines 472:0-472:24 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 472:0-472:24 -/
def Tuple (T1 T2 : Type) := T1 × T2
/- [no_nested_borrows::use_tuple_struct]:
- Source: 'src/no_nested_borrows.rs', lines 474:0-474:48 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 474:0-474:48 -/
def use_tuple_struct (x : Tuple U32 U32) : Result (Tuple U32 U32) :=
Result.ok (1#u32, x.#1)
/- [no_nested_borrows::create_tuple_struct]:
- Source: 'src/no_nested_borrows.rs', lines 478:0-478:61 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 478:0-478:61 -/
def create_tuple_struct (x : U32) (y : U64) : Result (Tuple U32 U64) :=
Result.ok (x, y)
/- [no_nested_borrows::IdType]
- Source: 'src/no_nested_borrows.rs', lines 483:0-483:20 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 483:0-483:20 -/
@[reducible] def IdType (T : Type) := T
/- [no_nested_borrows::use_id_type]:
- Source: 'src/no_nested_borrows.rs', lines 485:0-485:40 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 485:0-485:40 -/
def use_id_type (T : Type) (x : IdType T) : Result T :=
Result.ok x
/- [no_nested_borrows::create_id_type]:
- Source: 'src/no_nested_borrows.rs', lines 489:0-489:43 -/
+ Source: 'tests/src/no_nested_borrows.rs', lines 489:0-489:43 -/
def create_id_type (T : Type) (x : T) : Result (IdType T) :=
Result.ok x
diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
index 32203eca..bede3dd9 100644
--- a/tests/lean/Paper.lean
+++ b/tests/lean/Paper.lean
@@ -6,12 +6,12 @@ open Primitives
namespace paper
/- [paper::ref_incr]:
- Source: 'src/paper.rs', lines 4:0-4:28 -/
+ Source: 'tests/src/paper.rs', lines 4:0-4:28 -/
def ref_incr (x : I32) : Result I32 :=
x + 1#i32
/- [paper::test_incr]:
- Source: 'src/paper.rs', lines 8:0-8:18 -/
+ Source: 'tests/src/paper.rs', lines 8:0-8:18 -/
def test_incr : Result Unit :=
do
let x ← ref_incr 0#i32
@@ -23,7 +23,7 @@ def test_incr : Result Unit :=
#assert (test_incr == Result.ok ())
/- [paper::choose]:
- Source: 'src/paper.rs', lines 15:0-15:70 -/
+ Source: 'tests/src/paper.rs', lines 15:0-15:70 -/
def choose
(T : Type) (b : Bool) (x : T) (y : T) :
Result (T × (T → Result (T × T)))
@@ -35,7 +35,7 @@ def choose
Result.ok (y, back)
/- [paper::test_choose]:
- Source: 'src/paper.rs', lines 23:0-23:20 -/
+ Source: 'tests/src/paper.rs', lines 23:0-23:20 -/
def test_choose : Result Unit :=
do
let (z, choose_back) ← choose I32 true 0#i32 0#i32
@@ -55,13 +55,13 @@ def test_choose : Result Unit :=
#assert (test_choose == Result.ok ())
/- [paper::List]
- Source: 'src/paper.rs', lines 35:0-35:16 -/
+ Source: 'tests/src/paper.rs', lines 35:0-35:16 -/
inductive List (T : Type) :=
| Cons : T → List T → List T
| Nil : List T
/- [paper::list_nth_mut]:
- Source: 'src/paper.rs', lines 42:0-42:67 -/
+ Source: 'tests/src/paper.rs', lines 42:0-42:67 -/
divergent def list_nth_mut
(T : Type) (l : List T) (i : U32) : Result (T × (T → Result (List T))) :=
match l with
@@ -83,7 +83,7 @@ divergent def list_nth_mut
| List.Nil => Result.fail .panic
/- [paper::sum]:
- Source: 'src/paper.rs', lines 57:0-57:32 -/
+ Source: 'tests/src/paper.rs', lines 57:0-57:32 -/
divergent def sum (l : List I32) : Result I32 :=
match l with
| List.Cons x tl => do
@@ -92,7 +92,7 @@ divergent def sum (l : List I32) : Result I32 :=
| List.Nil => Result.ok 0#i32
/- [paper::test_nth]:
- Source: 'src/paper.rs', lines 68:0-68:17 -/
+ Source: 'tests/src/paper.rs', lines 68:0-68:17 -/
def test_nth : Result Unit :=
do
let l := List.Cons 3#i32 List.Nil
@@ -109,7 +109,7 @@ def test_nth : Result Unit :=
#assert (test_nth == Result.ok ())
/- [paper::call_choose]:
- Source: 'src/paper.rs', lines 76:0-76:44 -/
+ Source: 'tests/src/paper.rs', lines 76:0-76:44 -/
def call_choose (p : (U32 × U32)) : Result U32 :=
do
let (px, py) := p
diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean
index 09f41056..d1ed10d2 100644
--- a/tests/lean/PoloniusList.lean
+++ b/tests/lean/PoloniusList.lean
@@ -6,13 +6,13 @@ open Primitives
namespace polonius_list
/- [polonius_list::List]
- Source: 'src/polonius_list.rs', lines 3:0-3:16 -/
+ Source: 'tests/src/polonius_list.rs', lines 3:0-3:16 -/
inductive List (T : Type) :=
| Cons : T → List T → List T
| Nil : List T
/- [polonius_list::get_list_at_x]:
- Source: 'src/polonius_list.rs', lines 13:0-13:76 -/
+ Source: 'tests/src/polonius_list.rs', lines 13:0-13:76 -/
divergent def get_list_at_x
(ls : List U32) (x : U32) :
Result ((List U32) × (List U32 → Result (List U32)))
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
index 3746d494..32f84676 100644
--- a/tests/lean/Traits.lean
+++ b/tests/lean/Traits.lean
@@ -6,29 +6,29 @@ open Primitives
namespace traits
/- Trait declaration: [traits::BoolTrait]
- Source: 'src/traits.rs', lines 1:0-1:19 -/
+ Source: 'tests/src/traits.rs', lines 1:0-1:19 -/
structure BoolTrait (Self : Type) where
get_bool : Self → Result Bool
/- [traits::{(traits::BoolTrait for bool)}::get_bool]:
- Source: 'src/traits.rs', lines 12:4-12:30 -/
+ Source: 'tests/src/traits.rs', lines 12:4-12:30 -/
def BoolTraitBool.get_bool (self : Bool) : Result Bool :=
Result.ok self
/- Trait implementation: [traits::{(traits::BoolTrait for bool)}]
- Source: 'src/traits.rs', lines 11:0-11:23 -/
+ Source: 'tests/src/traits.rs', lines 11:0-11:23 -/
def BoolTraitBool : BoolTrait Bool := {
get_bool := BoolTraitBool.get_bool
}
/- [traits::BoolTrait::ret_true]:
- Source: 'src/traits.rs', lines 6:4-6:30 -/
+ Source: 'tests/src/traits.rs', lines 6:4-6:30 -/
def BoolTrait.ret_true
{Self : Type} (self_clause : BoolTrait Self) (self : Self) : Result Bool :=
Result.ok true
/- [traits::test_bool_trait_bool]:
- Source: 'src/traits.rs', lines 17:0-17:44 -/
+ Source: 'tests/src/traits.rs', lines 17:0-17:44 -/
def test_bool_trait_bool (x : Bool) : Result Bool :=
do
let b ← BoolTraitBool.get_bool x
@@ -37,20 +37,20 @@ def test_bool_trait_bool (x : Bool) : Result Bool :=
else Result.ok false
/- [traits::{(traits::BoolTrait for core::option::Option<T>)#1}::get_bool]:
- Source: 'src/traits.rs', lines 23:4-23:30 -/
+ Source: 'tests/src/traits.rs', lines 23:4-23:30 -/
def BoolTraitOption.get_bool (T : Type) (self : Option T) : Result Bool :=
match self with
| none => Result.ok false
| some _ => Result.ok true
/- Trait implementation: [traits::{(traits::BoolTrait for core::option::Option<T>)#1}]
- Source: 'src/traits.rs', lines 22:0-22:31 -/
+ Source: 'tests/src/traits.rs', lines 22:0-22:31 -/
def BoolTraitOption (T : Type) : BoolTrait (Option T) := {
get_bool := BoolTraitOption.get_bool T
}
/- [traits::test_bool_trait_option]:
- Source: 'src/traits.rs', lines 31:0-31:54 -/
+ Source: 'tests/src/traits.rs', lines 31:0-31:54 -/
def test_bool_trait_option (T : Type) (x : Option T) : Result Bool :=
do
let b ← BoolTraitOption.get_bool T x
@@ -59,29 +59,29 @@ def test_bool_trait_option (T : Type) (x : Option T) : Result Bool :=
else Result.ok false
/- [traits::test_bool_trait]:
- Source: 'src/traits.rs', lines 35:0-35:50 -/
+ Source: 'tests/src/traits.rs', lines 35:0-35:50 -/
def test_bool_trait
(T : Type) (BoolTraitInst : BoolTrait T) (x : T) : Result Bool :=
BoolTraitInst.get_bool x
/- Trait declaration: [traits::ToU64]
- Source: 'src/traits.rs', lines 39:0-39:15 -/
+ Source: 'tests/src/traits.rs', lines 39:0-39:15 -/
structure ToU64 (Self : Type) where
to_u64 : Self → Result U64
/- [traits::{(traits::ToU64 for u64)#2}::to_u64]:
- Source: 'src/traits.rs', lines 44:4-44:26 -/
+ Source: 'tests/src/traits.rs', lines 44:4-44:26 -/
def ToU64U64.to_u64 (self : U64) : Result U64 :=
Result.ok self
/- Trait implementation: [traits::{(traits::ToU64 for u64)#2}]
- Source: 'src/traits.rs', lines 43:0-43:18 -/
+ Source: 'tests/src/traits.rs', lines 43:0-43:18 -/
def ToU64U64 : ToU64 U64 := {
to_u64 := ToU64U64.to_u64
}
/- [traits::{(traits::ToU64 for (A, A))#3}::to_u64]:
- Source: 'src/traits.rs', lines 50:4-50:26 -/
+ Source: 'tests/src/traits.rs', lines 50:4-50:26 -/
def ToU64Pair.to_u64
(A : Type) (ToU64Inst : ToU64 A) (self : (A × A)) : Result U64 :=
do
@@ -91,78 +91,78 @@ def ToU64Pair.to_u64
i + i1
/- Trait implementation: [traits::{(traits::ToU64 for (A, A))#3}]
- Source: 'src/traits.rs', lines 49:0-49:31 -/
+ Source: 'tests/src/traits.rs', lines 49:0-49:31 -/
def ToU64Pair (A : Type) (ToU64Inst : ToU64 A) : ToU64 (A × A) := {
to_u64 := ToU64Pair.to_u64 A ToU64Inst
}
/- [traits::f]:
- Source: 'src/traits.rs', lines 55:0-55:36 -/
+ Source: 'tests/src/traits.rs', lines 55:0-55:36 -/
def f (T : Type) (ToU64Inst : ToU64 T) (x : (T × T)) : Result U64 :=
ToU64Pair.to_u64 T ToU64Inst x
/- [traits::g]:
- Source: 'src/traits.rs', lines 59:0-61:18 -/
+ Source: 'tests/src/traits.rs', lines 59:0-61:18 -/
def g
(T : Type) (ToU64PairInst : ToU64 (T × T)) (x : (T × T)) : Result U64 :=
ToU64PairInst.to_u64 x
/- [traits::h0]:
- Source: 'src/traits.rs', lines 66:0-66:24 -/
+ Source: 'tests/src/traits.rs', lines 66:0-66:24 -/
def h0 (x : U64) : Result U64 :=
ToU64U64.to_u64 x
/- [traits::Wrapper]
- Source: 'src/traits.rs', lines 70:0-70:21 -/
+ Source: 'tests/src/traits.rs', lines 70:0-70:21 -/
structure Wrapper (T : Type) where
x : T
/- [traits::{(traits::ToU64 for traits::Wrapper<T>)#4}::to_u64]:
- Source: 'src/traits.rs', lines 75:4-75:26 -/
+ Source: 'tests/src/traits.rs', lines 75:4-75:26 -/
def ToU64traitsWrapper.to_u64
(T : Type) (ToU64Inst : ToU64 T) (self : Wrapper T) : Result U64 :=
ToU64Inst.to_u64 self.x
/- Trait implementation: [traits::{(traits::ToU64 for traits::Wrapper<T>)#4}]
- Source: 'src/traits.rs', lines 74:0-74:35 -/
+ Source: 'tests/src/traits.rs', lines 74:0-74:35 -/
def ToU64traitsWrapper (T : Type) (ToU64Inst : ToU64 T) : ToU64 (Wrapper T)
:= {
to_u64 := ToU64traitsWrapper.to_u64 T ToU64Inst
}
/- [traits::h1]:
- Source: 'src/traits.rs', lines 80:0-80:33 -/
+ Source: 'tests/src/traits.rs', lines 80:0-80:33 -/
def h1 (x : Wrapper U64) : Result U64 :=
ToU64traitsWrapper.to_u64 U64 ToU64U64 x
/- [traits::h2]:
- Source: 'src/traits.rs', lines 84:0-84:41 -/
+ Source: 'tests/src/traits.rs', lines 84:0-84:41 -/
def h2 (T : Type) (ToU64Inst : ToU64 T) (x : Wrapper T) : Result U64 :=
ToU64traitsWrapper.to_u64 T ToU64Inst x
/- Trait declaration: [traits::ToType]
- Source: 'src/traits.rs', lines 88:0-88:19 -/
+ Source: 'tests/src/traits.rs', lines 88:0-88:19 -/
structure ToType (Self T : Type) where
to_type : Self → Result T
/- [traits::{(traits::ToType<bool> for u64)#5}::to_type]:
- Source: 'src/traits.rs', lines 93:4-93:28 -/
+ Source: 'tests/src/traits.rs', lines 93:4-93:28 -/
def ToTypeU64Bool.to_type (self : U64) : Result Bool :=
Result.ok (self > 0#u64)
/- Trait implementation: [traits::{(traits::ToType<bool> for u64)#5}]
- Source: 'src/traits.rs', lines 92:0-92:25 -/
+ Source: 'tests/src/traits.rs', lines 92:0-92:25 -/
def ToTypeU64Bool : ToType U64 Bool := {
to_type := ToTypeU64Bool.to_type
}
/- Trait declaration: [traits::OfType]
- Source: 'src/traits.rs', lines 98:0-98:16 -/
+ Source: 'tests/src/traits.rs', lines 98:0-98:16 -/
structure OfType (Self : Type) where
of_type : forall (T : Type) (ToTypeInst : ToType T Self), T → Result Self
/- [traits::h3]:
- Source: 'src/traits.rs', lines 104:0-104:50 -/
+ Source: 'tests/src/traits.rs', lines 104:0-104:50 -/
def h3
(T1 T2 : Type) (OfTypeInst : OfType T1) (ToTypeInst : ToType T2 T1)
(y : T2) :
@@ -171,13 +171,13 @@ def h3
OfTypeInst.of_type T2 ToTypeInst y
/- Trait declaration: [traits::OfTypeBis]
- Source: 'src/traits.rs', lines 109:0-109:36 -/
+ Source: 'tests/src/traits.rs', lines 109:0-109:36 -/
structure OfTypeBis (Self T : Type) where
ToTypeInst : ToType T Self
of_type : T → Result Self
/- [traits::h4]:
- Source: 'src/traits.rs', lines 118:0-118:57 -/
+ Source: 'tests/src/traits.rs', lines 118:0-118:57 -/
def h4
(T1 T2 : Type) (OfTypeBisInst : OfTypeBis T1 T2) (ToTypeInst : ToType T2 T1)
(y : T2) :
@@ -186,33 +186,33 @@ def h4
OfTypeBisInst.of_type y
/- [traits::TestType]
- Source: 'src/traits.rs', lines 122:0-122:22 -/
+ Source: 'tests/src/traits.rs', lines 122:0-122:22 -/
@[reducible] def TestType (T : Type) := T
/- [traits::{traits::TestType<T>#6}::test::TestType1]
- Source: 'src/traits.rs', lines 127:8-127:24 -/
+ Source: 'tests/src/traits.rs', lines 127:8-127:24 -/
@[reducible] def TestType.test.TestType1 := U64
/- Trait declaration: [traits::{traits::TestType<T>#6}::test::TestTrait]
- Source: 'src/traits.rs', lines 128:8-128:23 -/
+ Source: 'tests/src/traits.rs', lines 128:8-128:23 -/
structure TestType.test.TestTrait (Self : Type) where
test : Self → Result Bool
/- [traits::{traits::TestType<T>#6}::test::{(traits::{traits::TestType<T>#6}::test::TestTrait for traits::{traits::TestType<T>#6}::test::TestType1)}::test]:
- Source: 'src/traits.rs', lines 139:12-139:34 -/
+ Source: 'tests/src/traits.rs', lines 139:12-139:34 -/
def TestType.test.TestTraittraitsTestTypetestTestType1.test
(self : TestType.test.TestType1) : Result Bool :=
Result.ok (self > 1#u64)
/- Trait implementation: [traits::{traits::TestType<T>#6}::test::{(traits::{traits::TestType<T>#6}::test::TestTrait for traits::{traits::TestType<T>#6}::test::TestType1)}]
- Source: 'src/traits.rs', lines 138:8-138:36 -/
+ Source: 'tests/src/traits.rs', lines 138:8-138:36 -/
def TestType.test.TestTraittraitsTestTypetestTestType1 :
TestType.test.TestTrait TestType.test.TestType1 := {
test := TestType.test.TestTraittraitsTestTypetestTestType1.test
}
/- [traits::{traits::TestType<T>#6}::test]:
- Source: 'src/traits.rs', lines 126:4-126:36 -/
+ Source: 'tests/src/traits.rs', lines 126:4-126:36 -/
def TestType.test
(T : Type) (ToU64Inst : ToU64 T) (self : TestType T) (x : T) : Result Bool :=
do
@@ -222,11 +222,11 @@ def TestType.test
else Result.ok false
/- [traits::BoolWrapper]
- Source: 'src/traits.rs', lines 150:0-150:22 -/
+ Source: 'tests/src/traits.rs', lines 150:0-150:22 -/
@[reducible] def BoolWrapper := Bool
/- [traits::{(traits::ToType<T> for traits::BoolWrapper)#7}::to_type]:
- Source: 'src/traits.rs', lines 156:4-156:25 -/
+ Source: 'tests/src/traits.rs', lines 156:4-156:25 -/
def ToTypetraitsBoolWrapperT.to_type
(T : Type) (ToTypeBoolTInst : ToType Bool T) (self : BoolWrapper) :
Result T
@@ -234,21 +234,21 @@ def ToTypetraitsBoolWrapperT.to_type
ToTypeBoolTInst.to_type self
/- Trait implementation: [traits::{(traits::ToType<T> for traits::BoolWrapper)#7}]
- Source: 'src/traits.rs', lines 152:0-152:33 -/
+ Source: 'tests/src/traits.rs', lines 152:0-152:33 -/
def ToTypetraitsBoolWrapperT (T : Type) (ToTypeBoolTInst : ToType Bool T) :
ToType BoolWrapper T := {
to_type := ToTypetraitsBoolWrapperT.to_type T ToTypeBoolTInst
}
/- [traits::WithConstTy::LEN2]
- Source: 'src/traits.rs', lines 164:4-164:21 -/
+ Source: 'tests/src/traits.rs', lines 164:4-164:21 -/
def WithConstTy.LEN2_default_body (Self : Type) (LEN : Usize) : Result Usize :=
Result.ok 32#usize
def WithConstTy.LEN2_default (Self : Type) (LEN : Usize) : Usize :=
eval_global (WithConstTy.LEN2_default_body Self LEN)
/- Trait declaration: [traits::WithConstTy]
- Source: 'src/traits.rs', lines 161:0-161:39 -/
+ Source: 'tests/src/traits.rs', lines 161:0-161:39 -/
structure WithConstTy (Self : Type) (LEN : Usize) where
LEN1 : Usize
LEN2 : Usize
@@ -258,17 +258,17 @@ structure WithConstTy (Self : Type) (LEN : Usize) where
f : W → Array U8 LEN → Result W
/- [traits::{(traits::WithConstTy<32: usize> for bool)#8}::LEN1]
- Source: 'src/traits.rs', lines 175:4-175:21 -/
+ Source: 'tests/src/traits.rs', lines 175:4-175:21 -/
def WithConstTyBool32.LEN1_body : Result Usize := Result.ok 12#usize
def WithConstTyBool32.LEN1 : Usize := eval_global WithConstTyBool32.LEN1_body
/- [traits::{(traits::WithConstTy<32: usize> for bool)#8}::f]:
- Source: 'src/traits.rs', lines 180:4-180:39 -/
+ Source: 'tests/src/traits.rs', lines 180:4-180:39 -/
def WithConstTyBool32.f (i : U64) (a : Array U8 32#usize) : Result U64 :=
Result.ok i
/- Trait implementation: [traits::{(traits::WithConstTy<32: usize> for bool)#8}]
- Source: 'src/traits.rs', lines 174:0-174:29 -/
+ Source: 'tests/src/traits.rs', lines 174:0-174:29 -/
def WithConstTyBool32 : WithConstTy Bool 32#usize := {
LEN1 := WithConstTyBool32.LEN1
LEN2 := WithConstTy.LEN2_default Bool 32#usize
@@ -279,7 +279,7 @@ def WithConstTyBool32 : WithConstTy Bool 32#usize := {
}
/- [traits::use_with_const_ty1]:
- Source: 'src/traits.rs', lines 183:0-183:75 -/
+ Source: 'tests/src/traits.rs', lines 183:0-183:75 -/
def use_with_const_ty1
(H : Type) (LEN : Usize) (WithConstTyInst : WithConstTy H LEN) :
Result Usize
@@ -287,7 +287,7 @@ def use_with_const_ty1
Result.ok WithConstTyInst.LEN1
/- [traits::use_with_const_ty2]:
- Source: 'src/traits.rs', lines 187:0-187:73 -/
+ Source: 'tests/src/traits.rs', lines 187:0-187:73 -/
def use_with_const_ty2
(H : Type) (LEN : Usize) (WithConstTyInst : WithConstTy H LEN)
(w : WithConstTyInst.W) :
@@ -296,7 +296,7 @@ def use_with_const_ty2
Result.ok ()
/- [traits::use_with_const_ty3]:
- Source: 'src/traits.rs', lines 189:0-189:80 -/
+ Source: 'tests/src/traits.rs', lines 189:0-189:80 -/
def use_with_const_ty3
(H : Type) (LEN : Usize) (WithConstTyInst : WithConstTy H LEN)
(x : WithConstTyInst.W) :
@@ -305,12 +305,12 @@ def use_with_const_ty3
WithConstTyInst.W_clause_0.to_u64 x
/- [traits::test_where1]:
- Source: 'src/traits.rs', lines 193:0-193:40 -/
+ Source: 'tests/src/traits.rs', lines 193:0-193:40 -/
def test_where1 (T : Type) (_x : T) : Result Unit :=
Result.ok ()
/- [traits::test_where2]:
- Source: 'src/traits.rs', lines 194:0-194:57 -/
+ Source: 'tests/src/traits.rs', lines 194:0-194:57 -/
def test_where2
(T : Type) (WithConstTyT32Inst : WithConstTy T 32#usize) (_x : U32) :
Result Unit
@@ -318,30 +318,30 @@ def test_where2
Result.ok ()
/- Trait declaration: [traits::ParentTrait0]
- Source: 'src/traits.rs', lines 200:0-200:22 -/
+ Source: 'tests/src/traits.rs', lines 200:0-200:22 -/
structure ParentTrait0 (Self : Type) where
W : Type
get_name : Self → Result String
get_w : Self → Result W
/- Trait declaration: [traits::ParentTrait1]
- Source: 'src/traits.rs', lines 205:0-205:22 -/
+ Source: 'tests/src/traits.rs', lines 205:0-205:22 -/
structure ParentTrait1 (Self : Type) where
/- Trait declaration: [traits::ChildTrait]
- Source: 'src/traits.rs', lines 206:0-206:49 -/
+ Source: 'tests/src/traits.rs', lines 206:0-206:49 -/
structure ChildTrait (Self : Type) where
ParentTrait0Inst : ParentTrait0 Self
ParentTrait1Inst : ParentTrait1 Self
/- [traits::test_child_trait1]:
- Source: 'src/traits.rs', lines 209:0-209:56 -/
+ Source: 'tests/src/traits.rs', lines 209:0-209:56 -/
def test_child_trait1
(T : Type) (ChildTraitInst : ChildTrait T) (x : T) : Result String :=
ChildTraitInst.ParentTrait0Inst.get_name x
/- [traits::test_child_trait2]:
- Source: 'src/traits.rs', lines 213:0-213:54 -/
+ Source: 'tests/src/traits.rs', lines 213:0-213:54 -/
def test_child_trait2
(T : Type) (ChildTraitInst : ChildTrait T) (x : T) :
Result ChildTraitInst.ParentTrait0Inst.W
@@ -349,7 +349,7 @@ def test_child_trait2
ChildTraitInst.ParentTrait0Inst.get_w x
/- [traits::order1]:
- Source: 'src/traits.rs', lines 219:0-219:59 -/
+ Source: 'tests/src/traits.rs', lines 219:0-219:59 -/
def order1
(T U : Type) (ParentTrait0Inst : ParentTrait0 T) (ParentTrait0Inst1 :
ParentTrait0 U) :
@@ -358,28 +358,28 @@ def order1
Result.ok ()
/- Trait declaration: [traits::ChildTrait1]
- Source: 'src/traits.rs', lines 222:0-222:35 -/
+ Source: 'tests/src/traits.rs', lines 222:0-222:35 -/
structure ChildTrait1 (Self : Type) where
ParentTrait1Inst : ParentTrait1 Self
/- Trait implementation: [traits::{(traits::ParentTrait1 for usize)#9}]
- Source: 'src/traits.rs', lines 224:0-224:27 -/
+ Source: 'tests/src/traits.rs', lines 224:0-224:27 -/
def ParentTrait1Usize : ParentTrait1 Usize := {
}
/- Trait implementation: [traits::{(traits::ChildTrait1 for usize)#10}]
- Source: 'src/traits.rs', lines 225:0-225:26 -/
+ Source: 'tests/src/traits.rs', lines 225:0-225:26 -/
def ChildTrait1Usize : ChildTrait1 Usize := {
ParentTrait1Inst := ParentTrait1Usize
}
/- Trait declaration: [traits::Iterator]
- Source: 'src/traits.rs', lines 229:0-229:18 -/
+ Source: 'tests/src/traits.rs', lines 229:0-229:18 -/
structure Iterator (Self : Type) where
Item : Type
/- Trait declaration: [traits::IntoIterator]
- Source: 'src/traits.rs', lines 233:0-233:22 -/
+ Source: 'tests/src/traits.rs', lines 233:0-233:22 -/
structure IntoIterator (Self : Type) where
Item : Type
IntoIter : Type
@@ -387,106 +387,106 @@ structure IntoIterator (Self : Type) where
into_iter : Self → Result IntoIter
/- Trait declaration: [traits::FromResidual]
- Source: 'src/traits.rs', lines 250:0-250:21 -/
+ Source: 'tests/src/traits.rs', lines 250:0-250:21 -/
structure FromResidual (Self T : Type) where
/- Trait declaration: [traits::Try]
- Source: 'src/traits.rs', lines 246:0-246:48 -/
+ Source: 'tests/src/traits.rs', lines 246:0-246:48 -/
structure Try (Self : Type) where
Residual : Type
FromResidualSelftraitsTryResidualInst : FromResidual Self Residual
/- Trait declaration: [traits::WithTarget]
- Source: 'src/traits.rs', lines 252:0-252:20 -/
+ Source: 'tests/src/traits.rs', lines 252:0-252:20 -/
structure WithTarget (Self : Type) where
Target : Type
/- Trait declaration: [traits::ParentTrait2]
- Source: 'src/traits.rs', lines 256:0-256:22 -/
+ Source: 'tests/src/traits.rs', lines 256:0-256:22 -/
structure ParentTrait2 (Self : Type) where
U : Type
U_clause_0 : WithTarget U
/- Trait declaration: [traits::ChildTrait2]
- Source: 'src/traits.rs', lines 260:0-260:35 -/
+ Source: 'tests/src/traits.rs', lines 260:0-260:35 -/
structure ChildTrait2 (Self : Type) where
ParentTrait2Inst : ParentTrait2 Self
convert : ParentTrait2Inst.U → Result ParentTrait2Inst.U_clause_0.Target
/- Trait implementation: [traits::{(traits::WithTarget for u32)#11}]
- Source: 'src/traits.rs', lines 264:0-264:23 -/
+ Source: 'tests/src/traits.rs', lines 264:0-264:23 -/
def WithTargetU32 : WithTarget U32 := {
Target := U32
}
/- Trait implementation: [traits::{(traits::ParentTrait2 for u32)#12}]
- Source: 'src/traits.rs', lines 268:0-268:25 -/
+ Source: 'tests/src/traits.rs', lines 268:0-268:25 -/
def ParentTrait2U32 : ParentTrait2 U32 := {
U := U32
U_clause_0 := WithTargetU32
}
/- [traits::{(traits::ChildTrait2 for u32)#13}::convert]:
- Source: 'src/traits.rs', lines 273:4-273:29 -/
+ Source: 'tests/src/traits.rs', lines 273:4-273:29 -/
def ChildTrait2U32.convert (x : U32) : Result U32 :=
Result.ok x
/- Trait implementation: [traits::{(traits::ChildTrait2 for u32)#13}]
- Source: 'src/traits.rs', lines 272:0-272:24 -/
+ Source: 'tests/src/traits.rs', lines 272:0-272:24 -/
def ChildTrait2U32 : ChildTrait2 U32 := {
ParentTrait2Inst := ParentTrait2U32
convert := ChildTrait2U32.convert
}
/- Trait declaration: [traits::CFnOnce]
- Source: 'src/traits.rs', lines 286:0-286:23 -/
+ Source: 'tests/src/traits.rs', lines 286:0-286:23 -/
structure CFnOnce (Self Args : Type) where
Output : Type
call_once : Self → Args → Result Output
/- Trait declaration: [traits::CFnMut]
- Source: 'src/traits.rs', lines 292:0-292:37 -/
+ Source: 'tests/src/traits.rs', lines 292:0-292:37 -/
structure CFnMut (Self Args : Type) where
CFnOnceInst : CFnOnce Self Args
call_mut : Self → Args → Result (CFnOnceInst.Output × Self)
/- Trait declaration: [traits::CFn]
- Source: 'src/traits.rs', lines 296:0-296:33 -/
+ Source: 'tests/src/traits.rs', lines 296:0-296:33 -/
structure CFn (Self Args : Type) where
CFnMutInst : CFnMut Self Args
call : Self → Args → Result CFnMutInst.CFnOnceInst.Output
/- Trait declaration: [traits::GetTrait]
- Source: 'src/traits.rs', lines 300:0-300:18 -/
+ Source: 'tests/src/traits.rs', lines 300:0-300:18 -/
structure GetTrait (Self : Type) where
W : Type
get_w : Self → Result W
/- [traits::test_get_trait]:
- Source: 'src/traits.rs', lines 305:0-305:49 -/
+ Source: 'tests/src/traits.rs', lines 305:0-305:49 -/
def test_get_trait
(T : Type) (GetTraitInst : GetTrait T) (x : T) : Result GetTraitInst.W :=
GetTraitInst.get_w x
/- Trait declaration: [traits::Trait]
- Source: 'src/traits.rs', lines 310:0-310:15 -/
+ Source: 'tests/src/traits.rs', lines 310:0-310:15 -/
structure Trait (Self : Type) where
LEN : Usize
/- [traits::{(traits::Trait for @Array<T, N>)#14}::LEN]
- Source: 'src/traits.rs', lines 315:4-315:20 -/
+ Source: 'tests/src/traits.rs', lines 315:4-315:20 -/
def TraitArray.LEN_body (T : Type) (N : Usize) : Result Usize := Result.ok N
def TraitArray.LEN (T : Type) (N : Usize) : Usize :=
eval_global (TraitArray.LEN_body T N)
/- Trait implementation: [traits::{(traits::Trait for @Array<T, N>)#14}]
- Source: 'src/traits.rs', lines 314:0-314:40 -/
+ Source: 'tests/src/traits.rs', lines 314:0-314:40 -/
def TraitArray (T : Type) (N : Usize) : Trait (Array T N) := {
LEN := TraitArray.LEN T N
}
/- [traits::{(traits::Trait for traits::Wrapper<T>)#15}::LEN]
- Source: 'src/traits.rs', lines 319:4-319:20 -/
+ Source: 'tests/src/traits.rs', lines 319:4-319:20 -/
def TraittraitsWrapper.LEN_body (T : Type) (TraitInst : Trait T)
: Result Usize :=
Result.ok 0#usize
@@ -494,19 +494,19 @@ def TraittraitsWrapper.LEN (T : Type) (TraitInst : Trait T) : Usize :=
eval_global (TraittraitsWrapper.LEN_body T TraitInst)
/- Trait implementation: [traits::{(traits::Trait for traits::Wrapper<T>)#15}]
- Source: 'src/traits.rs', lines 318:0-318:35 -/
+ Source: 'tests/src/traits.rs', lines 318:0-318:35 -/
def TraittraitsWrapper (T : Type) (TraitInst : Trait T) : Trait (Wrapper T)
:= {
LEN := TraittraitsWrapper.LEN T TraitInst
}
/- [traits::use_wrapper_len]:
- Source: 'src/traits.rs', lines 322:0-322:43 -/
+ Source: 'tests/src/traits.rs', lines 322:0-322:43 -/
def use_wrapper_len (T : Type) (TraitInst : Trait T) : Result Usize :=
Result.ok (TraittraitsWrapper T TraitInst).LEN
/- [traits::Foo]
- Source: 'src/traits.rs', lines 326:0-326:20 -/
+ Source: 'tests/src/traits.rs', lines 326:0-326:20 -/
structure Foo (T U : Type) where
x : T
y : U
@@ -519,7 +519,7 @@ inductive core.result.Result (T E : Type) :=
| Err : E → core.result.Result T E
/- [traits::{traits::Foo<T, U>#16}::FOO]
- Source: 'src/traits.rs', lines 332:4-332:33 -/
+ Source: 'tests/src/traits.rs', lines 332:4-332:33 -/
def Foo.FOO_body (T U : Type) (TraitInst : Trait T)
: Result (core.result.Result T I32) :=
Result.ok (core.result.Result.Err 0#i32)
@@ -527,13 +527,13 @@ def Foo.FOO (T U : Type) (TraitInst : Trait T) : core.result.Result T I32 :=
eval_global (Foo.FOO_body T U TraitInst)
/- [traits::use_foo1]:
- Source: 'src/traits.rs', lines 335:0-335:48 -/
+ Source: 'tests/src/traits.rs', lines 335:0-335:48 -/
def use_foo1
(T U : Type) (TraitInst : Trait T) : Result (core.result.Result T I32) :=
Result.ok (Foo.FOO T U TraitInst)
/- [traits::use_foo2]:
- Source: 'src/traits.rs', lines 339:0-339:48 -/
+ Source: 'tests/src/traits.rs', lines 339:0-339:48 -/
def use_foo2
(T U : Type) (TraitInst : Trait U) : Result (core.result.Result U I32) :=
Result.ok (Foo.FOO U T TraitInst)