summaryrefslogtreecommitdiff
path: root/tests/lean
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean')
-rw-r--r--tests/lean/Arrays.lean225
-rw-r--r--tests/lean/Betree/Funs.lean22
-rw-r--r--tests/lean/Bitwise.lean8
-rw-r--r--tests/lean/Constants.lean28
-rw-r--r--tests/lean/Demo/Demo.lean28
-rw-r--r--tests/lean/External/Funs.lean2
-rw-r--r--tests/lean/Hashmap/Funs.lean62
-rw-r--r--tests/lean/Loops.lean94
-rw-r--r--tests/lean/Matches.lean6
-rw-r--r--tests/lean/NoNestedBorrows.lean138
-rw-r--r--tests/lean/Paper.lean34
-rw-r--r--tests/lean/Traits.lean24
12 files changed, 338 insertions, 333 deletions
diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index 70b4a26b..9748919e 100644
--- a/tests/lean/Arrays.lean
+++ b/tests/lean/Arrays.lean
@@ -14,34 +14,34 @@ inductive AB :=
/- [arrays::incr]:
Source: 'tests/src/arrays.rs', lines 11:0-11:24 -/
def incr (x : U32) : Result U32 :=
- x + 1u32
+ x + 1#u32
/- [arrays::array_to_shared_slice_]:
Source: 'tests/src/arrays.rs', lines 19:0-19:53 -/
def array_to_shared_slice_
- (T : Type) (s : Array T 32usize) : Result (Slice T) :=
- Array.to_slice T 32usize s
+ (T : Type) (s : Array T 32#usize) : Result (Slice T) :=
+ Array.to_slice T 32#usize s
/- [arrays::array_to_mut_slice_]:
Source: 'tests/src/arrays.rs', lines 24:0-24:58 -/
def array_to_mut_slice_
- (T : Type) (s : Array T 32usize) :
- Result ((Slice T) × (Slice T → Result (Array T 32usize)))
+ (T : Type) (s : Array T 32#usize) :
+ Result ((Slice T) × (Slice T → Result (Array T 32#usize)))
:=
- Array.to_slice_mut T 32usize s
+ Array.to_slice_mut T 32#usize s
/- [arrays::array_len]:
Source: 'tests/src/arrays.rs', lines 28:0-28:40 -/
-def array_len (T : Type) (s : Array T 32usize) : Result Usize :=
+def array_len (T : Type) (s : Array T 32#usize) : Result Usize :=
do
- let s1 ← Array.to_slice T 32usize s
+ let s1 ← Array.to_slice T 32#usize s
Result.ok (Slice.len T s1)
/- [arrays::shared_array_len]:
Source: 'tests/src/arrays.rs', lines 32:0-32:48 -/
-def shared_array_len (T : Type) (s : Array T 32usize) : Result Usize :=
+def shared_array_len (T : Type) (s : Array T 32#usize) : Result Usize :=
do
- let s1 ← Array.to_slice T 32usize s
+ let s1 ← Array.to_slice T 32#usize s
Result.ok (Slice.len T s1)
/- [arrays::shared_slice_len]:
@@ -52,26 +52,26 @@ def shared_slice_len (T : Type) (s : Slice T) : Result Usize :=
/- [arrays::index_array_shared]:
Source: 'tests/src/arrays.rs', lines 40:0-40:57 -/
def index_array_shared
- (T : Type) (s : Array T 32usize) (i : Usize) : Result T :=
- Array.index_usize T 32usize s i
+ (T : Type) (s : Array T 32#usize) (i : Usize) : Result T :=
+ Array.index_usize T 32#usize s i
/- [arrays::index_array_u32]:
Source: 'tests/src/arrays.rs', lines 47:0-47:53 -/
-def index_array_u32 (s : Array U32 32usize) (i : Usize) : Result U32 :=
- Array.index_usize U32 32usize s i
+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: 'tests/src/arrays.rs', lines 51:0-51:45 -/
-def index_array_copy (x : Array U32 32usize) : Result U32 :=
- Array.index_usize U32 32usize x 0usize
+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: 'tests/src/arrays.rs', lines 55:0-55:62 -/
def index_mut_array
- (T : Type) (s : Array T 32usize) (i : Usize) :
- Result (T × (T → Result (Array T 32usize)))
+ (T : Type) (s : Array T 32#usize) (i : Usize) :
+ Result (T × (T → Result (Array T 32#usize)))
:=
- Array.index_mut_usize T 32usize s i
+ Array.index_mut_usize T 32#usize s i
/- [arrays::index_slice]:
Source: 'tests/src/arrays.rs', lines 59:0-59:46 -/
@@ -109,22 +109,22 @@ def slice_subslice_mut_
/- [arrays::array_to_slice_shared_]:
Source: 'tests/src/arrays.rs', lines 75:0-75:54 -/
-def array_to_slice_shared_ (x : Array U32 32usize) : Result (Slice U32) :=
- Array.to_slice U32 32usize x
+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: 'tests/src/arrays.rs', lines 79:0-79:59 -/
def array_to_slice_mut_
- (x : Array U32 32usize) :
- Result ((Slice U32) × (Slice U32 → Result (Array U32 32usize)))
+ (x : Array U32 32#usize) :
+ Result ((Slice U32) × (Slice U32 → Result (Array U32 32#usize)))
:=
- Array.to_slice_mut U32 32usize x
+ Array.to_slice_mut U32 32#usize x
/- [arrays::array_subslice_shared_]:
Source: 'tests/src/arrays.rs', lines 83:0-83:74 -/
def array_subslice_shared_
- (x : Array U32 32usize) (y : Usize) (z : Usize) : Result (Slice U32) :=
- core.array.Array.index U32 (core.ops.range.Range Usize) 32usize
+ (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)
(core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) x
{ start := y, end_ := z }
@@ -132,12 +132,12 @@ def array_subslice_shared_
/- [arrays::array_subslice_mut_]:
Source: 'tests/src/arrays.rs', lines 87:0-87:79 -/
def array_subslice_mut_
- (x : Array U32 32usize) (y : Usize) (z : Usize) :
- Result ((Slice U32) × (Slice U32 → Result (Array U32 32usize)))
+ (x : Array U32 32#usize) (y : Usize) (z : Usize) :
+ Result ((Slice U32) × (Slice U32 → Result (Array U32 32#usize)))
:=
do
let (s, index_mut_back) ←
- core.array.Array.index_mut U32 (core.ops.range.Range Usize) 32usize
+ core.array.Array.index_mut U32 (core.ops.range.Range Usize) 32#usize
(core.ops.index.IndexMutSliceTIInst U32 (core.ops.range.Range Usize)
(core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) x
{ start := y, end_ := z }
@@ -146,50 +146,50 @@ def array_subslice_mut_
/- [arrays::index_slice_0]:
Source: 'tests/src/arrays.rs', lines 91:0-91:38 -/
def index_slice_0 (T : Type) (s : Slice T) : Result T :=
- Slice.index_usize T s 0usize
+ Slice.index_usize T s 0#usize
/- [arrays::index_array_0]:
Source: 'tests/src/arrays.rs', lines 95:0-95:42 -/
-def index_array_0 (T : Type) (s : Array T 32usize) : Result T :=
- Array.index_usize T 32usize s 0usize
+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: 'tests/src/arrays.rs', lines 106:0-106:71 -/
def index_index_array
- (s : Array (Array U32 32usize) 32usize) (i : Usize) (j : Usize) :
+ (s : Array (Array U32 32#usize) 32#usize) (i : Usize) (j : Usize) :
Result U32
:=
do
- let a ← Array.index_usize (Array U32 32usize) 32usize s i
- Array.index_usize U32 32usize a j
+ let a ← Array.index_usize (Array U32 32#usize) 32#usize s i
+ Array.index_usize U32 32#usize a j
/- [arrays::update_update_array]:
Source: 'tests/src/arrays.rs', lines 117:0-117:70 -/
def update_update_array
- (s : Array (Array U32 32usize) 32usize) (i : Usize) (j : Usize) :
+ (s : Array (Array U32 32#usize) 32#usize) (i : Usize) (j : Usize) :
Result Unit
:=
do
let (a, index_mut_back) ←
- Array.index_mut_usize (Array U32 32usize) 32usize s i
- let (_, index_mut_back1) ← Array.index_mut_usize U32 32usize a j
- let a1 ← index_mut_back1 0u32
+ Array.index_mut_usize (Array U32 32#usize) 32#usize s i
+ let (_, index_mut_back1) ← Array.index_mut_usize U32 32#usize a j
+ let a1 ← index_mut_back1 0#u32
let _ ← index_mut_back a1
Result.ok ()
/- [arrays::array_local_deep_copy]:
Source: 'tests/src/arrays.rs', lines 121:0-121:43 -/
-def array_local_deep_copy (x : Array U32 32usize) : Result Unit :=
+def array_local_deep_copy (x : Array U32 32#usize) : Result Unit :=
Result.ok ()
/- [arrays::take_array]:
Source: 'tests/src/arrays.rs', lines 125:0-125:30 -/
-def take_array (a : Array U32 2usize) : Result Unit :=
+def take_array (a : Array U32 2#usize) : Result Unit :=
Result.ok ()
/- [arrays::take_array_borrow]:
Source: 'tests/src/arrays.rs', lines 126:0-126:38 -/
-def take_array_borrow (a : Array U32 2usize) : Result Unit :=
+def take_array_borrow (a : Array U32 2#usize) : Result Unit :=
Result.ok ()
/- [arrays::take_slice]:
@@ -204,67 +204,70 @@ def take_mut_slice (s : Slice U32) : Result (Slice U32) :=
/- [arrays::const_array]:
Source: 'tests/src/arrays.rs', lines 130:0-130:32 -/
-def const_array : Result (Array U32 2usize) :=
- Result.ok (Array.make U32 2usize [ 0u32, 0u32 ])
+def const_array : Result (Array U32 2#usize) :=
+ Result.ok (Array.make U32 2#usize [ 0#u32, 0#u32 ])
/- [arrays::const_slice]:
Source: 'tests/src/arrays.rs', lines 134:0-134:20 -/
def const_slice : Result Unit :=
do
- let _ ← Array.to_slice U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ])
+ let _ ←
+ Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
Result.ok ()
/- [arrays::take_all]:
Source: 'tests/src/arrays.rs', lines 144:0-144:17 -/
def take_all : Result Unit :=
do
- let _ ← take_array (Array.make U32 2usize [ 0u32, 0u32 ])
- let _ ← take_array (Array.make U32 2usize [ 0u32, 0u32 ])
- let _ ← take_array_borrow (Array.make U32 2usize [ 0u32, 0u32 ])
- let s ← Array.to_slice U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ])
+ let _ ← take_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+ let _ ← take_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+ let _ ← take_array_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+ let s ←
+ Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
let _ ← take_slice s
let (s1, to_slice_mut_back) ←
- Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ])
+ Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
let s2 ← take_mut_slice s1
let _ ← to_slice_mut_back s2
Result.ok ()
/- [arrays::index_array]:
Source: 'tests/src/arrays.rs', lines 158:0-158:38 -/
-def index_array (x : Array U32 2usize) : Result U32 :=
- Array.index_usize U32 2usize x 0usize
+def index_array (x : Array U32 2#usize) : Result U32 :=
+ Array.index_usize U32 2#usize x 0#usize
/- [arrays::index_array_borrow]:
Source: 'tests/src/arrays.rs', lines 161:0-161:46 -/
-def index_array_borrow (x : Array U32 2usize) : Result U32 :=
- Array.index_usize U32 2usize x 0usize
+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: 'tests/src/arrays.rs', lines 165:0-165:42 -/
def index_slice_u32_0 (x : Slice U32) : Result U32 :=
- Slice.index_usize U32 x 0usize
+ Slice.index_usize U32 x 0#usize
/- [arrays::index_mut_slice_u32_0]:
Source: 'tests/src/arrays.rs', lines 169:0-169:50 -/
def index_mut_slice_u32_0 (x : Slice U32) : Result (U32 × (Slice U32)) :=
do
- let i ← Slice.index_usize U32 x 0usize
+ let i ← Slice.index_usize U32 x 0#usize
Result.ok (i, x)
/- [arrays::index_all]:
Source: 'tests/src/arrays.rs', lines 173:0-173:25 -/
def index_all : Result U32 :=
do
- let i ← index_array (Array.make U32 2usize [ 0u32, 0u32 ])
- let i1 ← index_array (Array.make U32 2usize [ 0u32, 0u32 ])
+ let i ← index_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+ let i1 ← index_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
let i2 ← i + i1
- let i3 ← index_array_borrow (Array.make U32 2usize [ 0u32, 0u32 ])
+ let i3 ← index_array_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ])
let i4 ← i2 + i3
- let s ← Array.to_slice U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ])
+ let s ←
+ Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
let i5 ← index_slice_u32_0 s
let i6 ← i4 + i5
let (s1, to_slice_mut_back) ←
- Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ])
+ Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
let (i7, s2) ← index_mut_slice_u32_0 s1
let i8 ← i6 + i7
let _ ← to_slice_mut_back s2
@@ -272,35 +275,35 @@ def index_all : Result U32 :=
/- [arrays::update_array]:
Source: 'tests/src/arrays.rs', lines 187:0-187:36 -/
-def update_array (x : Array U32 2usize) : Result Unit :=
+def update_array (x : Array U32 2#usize) : Result Unit :=
do
- let (_, index_mut_back) ← Array.index_mut_usize U32 2usize x 0usize
- let _ ← index_mut_back 1u32
+ let (_, index_mut_back) ← Array.index_mut_usize U32 2#usize x 0#usize
+ let _ ← index_mut_back 1#u32
Result.ok ()
/- [arrays::update_array_mut_borrow]:
Source: 'tests/src/arrays.rs', lines 190:0-190:48 -/
def update_array_mut_borrow
- (x : Array U32 2usize) : Result (Array U32 2usize) :=
+ (x : Array U32 2#usize) : Result (Array U32 2#usize) :=
do
- let (_, index_mut_back) ← Array.index_mut_usize U32 2usize x 0usize
- index_mut_back 1u32
+ let (_, index_mut_back) ← Array.index_mut_usize U32 2#usize x 0#usize
+ index_mut_back 1#u32
/- [arrays::update_mut_slice]:
Source: 'tests/src/arrays.rs', lines 193:0-193:38 -/
def update_mut_slice (x : Slice U32) : Result (Slice U32) :=
do
- let (_, index_mut_back) ← Slice.index_mut_usize U32 x 0usize
- index_mut_back 1u32
+ let (_, index_mut_back) ← Slice.index_mut_usize U32 x 0#usize
+ index_mut_back 1#u32
/- [arrays::update_all]:
Source: 'tests/src/arrays.rs', lines 197:0-197:19 -/
def update_all : Result Unit :=
do
- let _ ← update_array (Array.make U32 2usize [ 0u32, 0u32 ])
- let _ ← update_array (Array.make U32 2usize [ 0u32, 0u32 ])
- let x ← update_array_mut_borrow (Array.make U32 2usize [ 0u32, 0u32 ])
- let (s, to_slice_mut_back) ← Array.to_slice_mut U32 2usize x
+ let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+ let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+ let x ← update_array_mut_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+ let (s, to_slice_mut_back) ← Array.to_slice_mut U32 2#usize x
let s1 ← update_mut_slice s
let _ ← to_slice_mut_back s1
Result.ok ()
@@ -310,37 +313,37 @@ def update_all : Result Unit :=
def range_all : Result Unit :=
do
let (s, index_mut_back) ←
- core.array.Array.index_mut U32 (core.ops.range.Range Usize) 4usize
+ core.array.Array.index_mut U32 (core.ops.range.Range Usize) 4#usize
(core.ops.index.IndexMutSliceTIInst U32 (core.ops.range.Range Usize)
(core.slice.index.SliceIndexRangeUsizeSliceTInst U32))
- (Array.make U32 4usize [ 0u32, 0u32, 0u32, 0u32 ])
- { start := 1usize, end_ := 3usize }
+ (Array.make U32 4#usize [ 0#u32, 0#u32, 0#u32, 0#u32 ])
+ { start := 1#usize, end_ := 3#usize }
let s1 ← update_mut_slice s
let _ ← index_mut_back s1
Result.ok ()
/- [arrays::deref_array_borrow]:
Source: 'tests/src/arrays.rs', lines 217:0-217:46 -/
-def deref_array_borrow (x : Array U32 2usize) : Result U32 :=
- Array.index_usize U32 2usize x 0usize
+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: 'tests/src/arrays.rs', lines 222:0-222:54 -/
def deref_array_mut_borrow
- (x : Array U32 2usize) : Result (U32 × (Array U32 2usize)) :=
+ (x : Array U32 2#usize) : Result (U32 × (Array U32 2#usize)) :=
do
- let i ← Array.index_usize U32 2usize x 0usize
+ let i ← Array.index_usize U32 2#usize x 0#usize
Result.ok (i, x)
/- [arrays::take_array_t]:
Source: 'tests/src/arrays.rs', lines 230:0-230:31 -/
-def take_array_t (a : Array AB 2usize) : Result Unit :=
+def take_array_t (a : Array AB 2#usize) : Result Unit :=
Result.ok ()
/- [arrays::non_copyable_array]:
Source: 'tests/src/arrays.rs', lines 232:0-232:27 -/
def non_copyable_array : Result Unit :=
- take_array_t (Array.make AB 2usize [ AB.A, AB.B ])
+ take_array_t (Array.make AB 2#usize [ AB.A, AB.B ])
/- [arrays::sum]: loop 0:
Source: 'tests/src/arrays.rs', lines 245:0-253:1 -/
@@ -351,14 +354,14 @@ divergent def sum_loop (s : Slice U32) (sum1 : U32) (i : Usize) : Result U32 :=
do
let i2 ← Slice.index_usize U32 s i
let sum3 ← sum1 + i2
- let i3 ← i + 1usize
+ let i3 ← i + 1#usize
sum_loop s sum3 i3
else Result.ok sum1
/- [arrays::sum]:
Source: 'tests/src/arrays.rs', lines 245:0-245:28 -/
def sum (s : Slice U32) : Result U32 :=
- sum_loop s 0u32 0usize
+ sum_loop s 0#u32 0#usize
/- [arrays::sum2]: loop 0:
Source: 'tests/src/arrays.rs', lines 255:0-264:1 -/
@@ -372,7 +375,7 @@ divergent def sum2_loop
let i3 ← Slice.index_usize U32 s2 i
let i4 ← i2 + i3
let sum3 ← sum1 + i4
- let i5 ← i + 1usize
+ let i5 ← i + 1#usize
sum2_loop s s2 sum3 i5
else Result.ok sum1
@@ -382,7 +385,7 @@ def sum2 (s : Slice U32) (s2 : Slice U32) : Result U32 :=
let i := Slice.len U32 s
let i1 := Slice.len U32 s2
if i = i1
- then sum2_loop s s2 0u32 0usize
+ then sum2_loop s s2 0#u32 0#usize
else Result.fail .panic
/- [arrays::f0]:
@@ -390,9 +393,9 @@ def sum2 (s : Slice U32) (s2 : Slice U32) : Result U32 :=
def f0 : Result Unit :=
do
let (s, to_slice_mut_back) ←
- Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 1u32, 2u32 ])
- let (_, index_mut_back) ← Slice.index_mut_usize U32 s 0usize
- let s1 ← index_mut_back 1u32
+ Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ])
+ let (_, index_mut_back) ← Slice.index_mut_usize U32 s 0#usize
+ let s1 ← index_mut_back 1#u32
let _ ← to_slice_mut_back s1
Result.ok ()
@@ -401,9 +404,9 @@ def f0 : Result Unit :=
def f1 : Result Unit :=
do
let (_, index_mut_back) ←
- Array.index_mut_usize U32 2usize (Array.make U32 2usize [ 1u32, 2u32 ])
- 0usize
- let _ ← index_mut_back 1u32
+ Array.index_mut_usize U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ])
+ 0#usize
+ let _ ← index_mut_back 1#u32
Result.ok ()
/- [arrays::f2]:
@@ -413,8 +416,8 @@ def f2 (i : U32) : Result Unit :=
/- [arrays::f4]:
Source: 'tests/src/arrays.rs', lines 285:0-285:54 -/
-def f4 (x : Array U32 32usize) (y : Usize) (z : Usize) : Result (Slice U32) :=
- core.array.Array.index U32 (core.ops.range.Range Usize) 32usize
+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)
(core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) x
{ start := y, end_ := z }
@@ -424,32 +427,34 @@ def f4 (x : Array U32 32usize) (y : Usize) (z : Usize) : Result (Slice U32) :=
def f3 : Result U32 :=
do
let i ←
- Array.index_usize U32 2usize (Array.make U32 2usize [ 1u32, 2u32 ]) 0usize
+ Array.index_usize U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ])
+ 0#usize
let _ ← f2 i
- let b := Array.repeat U32 32usize 0u32
- let s ← Array.to_slice U32 2usize (Array.make U32 2usize [ 1u32, 2u32 ])
- let s1 ← f4 b 16usize 18usize
+ let b := Array.repeat U32 32#usize 0#u32
+ let s ←
+ Array.to_slice U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ])
+ let s1 ← f4 b 16#usize 18#usize
sum2 s s1
/- [arrays::SZ]
Source: 'tests/src/arrays.rs', lines 289:0-289:19 -/
-def SZ_body : Result Usize := Result.ok 32usize
+def SZ_body : Result Usize := Result.ok 32#usize
def SZ : Usize := eval_global SZ_body
/- [arrays::f5]:
Source: 'tests/src/arrays.rs', lines 292:0-292:31 -/
-def f5 (x : Array U32 32usize) : Result U32 :=
- Array.index_usize U32 32usize x 0usize
+def f5 (x : Array U32 32#usize) : Result U32 :=
+ Array.index_usize U32 32#usize x 0#usize
/- [arrays::ite]:
Source: 'tests/src/arrays.rs', lines 297:0-297:12 -/
def ite : Result Unit :=
do
let (s, to_slice_mut_back) ←
- Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ])
+ Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
let (_, s1) ← index_mut_slice_u32_0 s
let (s2, to_slice_mut_back1) ←
- Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ])
+ Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
let (_, s3) ← index_mut_slice_u32_0 s2
let _ ← to_slice_mut_back1 s3
let _ ← to_slice_mut_back s1
@@ -463,8 +468,8 @@ divergent def zero_slice_loop
then
do
let (_, index_mut_back) ← Slice.index_mut_usize U8 a i
- let i1 ← i + 1usize
- let a1 ← index_mut_back 0u8
+ let i1 ← i + 1#usize
+ let a1 ← index_mut_back 0#u8
zero_slice_loop a1 i1 len
else Result.ok a
@@ -472,14 +477,14 @@ divergent def zero_slice_loop
Source: 'tests/src/arrays.rs', lines 306:0-306:31 -/
def zero_slice (a : Slice U8) : Result (Slice U8) :=
let len := Slice.len U8 a
- zero_slice_loop a 0usize len
+ zero_slice_loop a 0#usize len
/- [arrays::iter_mut_slice]: loop 0:
Source: 'tests/src/arrays.rs', lines 315:0-321:1 -/
divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit :=
if i < len
then do
- let i1 ← i + 1usize
+ let i1 ← i + 1#usize
iter_mut_slice_loop len i1
else Result.ok ()
@@ -488,7 +493,7 @@ divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit :=
def iter_mut_slice (a : Slice U8) : Result (Slice U8) :=
do
let len := Slice.len U8 a
- let _ ← iter_mut_slice_loop len 0usize
+ let _ ← iter_mut_slice_loop len 0#usize
Result.ok a
/- [arrays::sum_mut_slice]: loop 0:
@@ -501,7 +506,7 @@ divergent def sum_mut_slice_loop
do
let i2 ← Slice.index_usize U32 a i
let s1 ← s + i2
- let i3 ← i + 1usize
+ let i3 ← i + 1#usize
sum_mut_slice_loop a i3 s1
else Result.ok s
@@ -509,7 +514,7 @@ divergent def sum_mut_slice_loop
Source: 'tests/src/arrays.rs', lines 323:0-323:42 -/
def sum_mut_slice (a : Slice U32) : Result (U32 × (Slice U32)) :=
do
- let i ← sum_mut_slice_loop a 0usize 0u32
+ let i ← sum_mut_slice_loop a 0#usize 0#u32
Result.ok (i, a)
end arrays
diff --git a/tests/lean/Betree/Funs.lean b/tests/lean/Betree/Funs.lean
index 74344e01..7d8b4714 100644
--- a/tests/lean/Betree/Funs.lean
+++ b/tests/lean/Betree/Funs.lean
@@ -41,20 +41,20 @@ def betree.store_leaf_node
Source: 'src/betree.rs', lines 55:0-55:48 -/
def betree.fresh_node_id (counter : U64) : Result (U64 × U64) :=
do
- let counter1 ← counter + 1u64
+ let counter1 ← counter + 1#u64
Result.ok (counter, counter1)
/- [betree::betree::{betree::betree::NodeIdCounter}::new]:
Source: 'src/betree.rs', lines 206:4-206:20 -/
def betree.NodeIdCounter.new : Result betree.NodeIdCounter :=
- Result.ok { next_node_id := 0u64 }
+ Result.ok { next_node_id := 0#u64 }
/- [betree::betree::{betree::betree::NodeIdCounter}::fresh_id]:
Source: 'src/betree.rs', lines 210:4-210:36 -/
def betree.NodeIdCounter.fresh_id
(self : betree.NodeIdCounter) : Result (U64 × betree.NodeIdCounter) :=
do
- let i ← self.next_node_id + 1u64
+ let i ← self.next_node_id + 1#u64
Result.ok (self.next_node_id, { next_node_id := i })
/- [betree::betree::upsert_update]:
@@ -65,7 +65,7 @@ def betree.upsert_update
| none =>
match st with
| betree.UpsertFunState.Add v => Result.ok v
- | betree.UpsertFunState.Sub _ => Result.ok 0u64
+ | betree.UpsertFunState.Sub _ => Result.ok 0#u64
| some prev1 =>
match st with
| betree.UpsertFunState.Add v =>
@@ -77,7 +77,7 @@ def betree.upsert_update
| betree.UpsertFunState.Sub v =>
if prev1 >= v
then prev1 - v
- else Result.ok 0u64
+ else Result.ok 0#u64
/- [betree::betree::{betree::betree::List<T>#1}::len]: loop 0:
Source: 'src/betree.rs', lines 276:4-284:5 -/
@@ -86,14 +86,14 @@ divergent def betree.List.len_loop
match self with
| betree.List.Cons _ tl =>
do
- let len1 ← len + 1u64
+ let len1 ← len + 1#u64
betree.List.len_loop T tl len1
| betree.List.Nil => Result.ok len
/- [betree::betree::{betree::betree::List<T>#1}::len]:
Source: 'src/betree.rs', lines 276:4-276:24 -/
def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
- betree.List.len_loop T self 0u64
+ betree.List.len_loop T self 0#u64
/- [betree::betree::{betree::betree::List<T>#1}::reverse]: loop 0:
Source: 'src/betree.rs', lines 304:4-312:5 -/
@@ -118,12 +118,12 @@ divergent def betree.List.split_at_loop
(T : Type) (n : U64) (beg : betree.List T) (self : betree.List T) :
Result ((betree.List T) × (betree.List T))
:=
- if n > 0u64
+ if n > 0#u64
then
match self with
| betree.List.Cons hd tl =>
do
- let n1 ← n - 1u64
+ let n1 ← n - 1#u64
betree.List.split_at_loop T n1 (betree.List.Cons hd beg) tl
| betree.List.Nil => Result.fail .panic
else do
@@ -706,7 +706,7 @@ divergent def betree.Node.apply_messages
let (st1, content) ← betree.load_leaf_node node.id st
let content1 ← betree.Node.apply_messages_to_leaf content msgs
let len ← betree.List.len (U64 × U64) content1
- let i ← 2u64 * params.split_size
+ let i ← 2#u64 * params.split_size
if len >= i
then
do
@@ -751,7 +751,7 @@ def betree.BeTree.new
{
params := { min_flush_size := min_flush_size, split_size := split_size },
node_id_cnt := node_id_cnt1,
- root := (betree.Node.Leaf { id := id, size := 0u64 })
+ root := (betree.Node.Leaf { id := id, size := 0#u64 })
})
/- [betree::betree::{betree::betree::BeTree#6}::apply]:
diff --git a/tests/lean/Bitwise.lean b/tests/lean/Bitwise.lean
index 8884d309..23ec66b4 100644
--- a/tests/lean/Bitwise.lean
+++ b/tests/lean/Bitwise.lean
@@ -9,15 +9,15 @@ namespace bitwise
Source: 'tests/src/bitwise.rs', lines 5:0-5:31 -/
def shift_u32 (a : U32) : Result U32 :=
do
- let t ← a >>> 16usize
- t <<< 16usize
+ let t ← a >>> 16#usize
+ t <<< 16#usize
/- [bitwise::shift_i32]:
Source: 'tests/src/bitwise.rs', lines 12:0-12:31 -/
def shift_i32 (a : I32) : Result I32 :=
do
- let t ← a >>> 16isize
- t <<< 16isize
+ let t ← a >>> 16#isize
+ t <<< 16#isize
/- [bitwise::xor_u32]:
Source: 'tests/src/bitwise.rs', lines 19:0-19:37 -/
diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean
index a72ac98d..ecb91c16 100644
--- a/tests/lean/Constants.lean
+++ b/tests/lean/Constants.lean
@@ -7,7 +7,7 @@ namespace constants
/- [constants::X0]
Source: 'tests/src/constants.rs', lines 8:0-8:17 -/
-def X0_body : Result U32 := Result.ok 0u32
+def X0_body : Result U32 := Result.ok 0#u32
def X0 : U32 := eval_global X0_body
/- [constants::X1]
@@ -17,17 +17,17 @@ def X1 : U32 := eval_global X1_body
/- [constants::X2]
Source: 'tests/src/constants.rs', lines 13:0-13:17 -/
-def X2_body : Result U32 := Result.ok 3u32
+def X2_body : Result U32 := Result.ok 3#u32
def X2 : U32 := eval_global X2_body
/- [constants::incr]:
Source: 'tests/src/constants.rs', lines 20:0-20:32 -/
def incr (n : U32) : Result U32 :=
- n + 1u32
+ n + 1#u32
/- [constants::X3]
Source: 'tests/src/constants.rs', lines 18:0-18:17 -/
-def X3_body : Result U32 := incr 32u32
+def X3_body : Result U32 := incr 32#u32
def X3 : U32 := eval_global X3_body
/- [constants::mk_pair0]:
@@ -48,22 +48,22 @@ def mk_pair1 (x : U32) (y : U32) : Result (Pair U32 U32) :=
/- [constants::P0]
Source: 'tests/src/constants.rs', lines 34:0-34:24 -/
-def P0_body : Result (U32 × U32) := mk_pair0 0u32 1u32
+def P0_body : Result (U32 × U32) := mk_pair0 0#u32 1#u32
def P0 : (U32 × U32) := eval_global P0_body
/- [constants::P1]
Source: 'tests/src/constants.rs', lines 35:0-35:28 -/
-def P1_body : Result (Pair U32 U32) := mk_pair1 0u32 1u32
+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: 'tests/src/constants.rs', lines 36:0-36:24 -/
-def P2_body : Result (U32 × U32) := Result.ok (0u32, 1u32)
+def P2_body : Result (U32 × U32) := Result.ok (0#u32, 1#u32)
def P2 : (U32 × U32) := eval_global P2_body
/- [constants::P3]
Source: 'tests/src/constants.rs', lines 37:0-37:28 -/
-def P3_body : Result (Pair U32 U32) := Result.ok { x := 0u32, y := 1u32 }
+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]
@@ -78,7 +78,7 @@ def Wrap.new (T : Type) (value : T) : Result (Wrap T) :=
/- [constants::Y]
Source: 'tests/src/constants.rs', lines 44:0-44:22 -/
-def Y_body : Result (Wrap I32) := Wrap.new I32 2i32
+def Y_body : Result (Wrap I32) := Wrap.new I32 2#i32
def Y : Wrap I32 := eval_global Y_body
/- [constants::unwrap_y]:
@@ -93,7 +93,7 @@ def YVAL : I32 := eval_global YVAL_body
/- [constants::get_z1::Z1]
Source: 'tests/src/constants.rs', lines 65:4-65:17 -/
-def get_z1.Z1_body : Result I32 := Result.ok 3i32
+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]:
@@ -108,7 +108,7 @@ def add (a : I32) (b : I32) : Result I32 :=
/- [constants::Q1]
Source: 'tests/src/constants.rs', lines 77:0-77:17 -/
-def Q1_body : Result I32 := Result.ok 5i32
+def Q1_body : Result I32 := Result.ok 5#i32
def Q1 : I32 := eval_global Q1_body
/- [constants::Q2]
@@ -118,7 +118,7 @@ def Q2 : I32 := eval_global Q2_body
/- [constants::Q3]
Source: 'tests/src/constants.rs', lines 79:0-79:17 -/
-def Q3_body : Result I32 := add Q2 3i32
+def Q3_body : Result I32 := add Q2 3#i32
def Q3 : I32 := eval_global Q3_body
/- [constants::get_z2]:
@@ -131,7 +131,7 @@ def get_z2 : Result I32 :=
/- [constants::S1]
Source: 'tests/src/constants.rs', lines 83:0-83:18 -/
-def S1_body : Result U32 := Result.ok 6u32
+def S1_body : Result U32 := Result.ok 6#u32
def S1 : U32 := eval_global S1_body
/- [constants::S2]
@@ -146,7 +146,7 @@ def S3 : Pair U32 U32 := eval_global S3_body
/- [constants::S4]
Source: 'tests/src/constants.rs', lines 86:0-86:29 -/
-def S4_body : Result (Pair U32 U32) := mk_pair1 7u32 8u32
+def S4_body : Result (Pair U32 U32) := mk_pair1 7#u32 8#u32
def S4 : Pair U32 U32 := eval_global S4_body
/- [constants::V]
diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
index 9d8b085c..48ac2062 100644
--- a/tests/lean/Demo/Demo.lean
+++ b/tests/lean/Demo/Demo.lean
@@ -22,7 +22,7 @@ def choose
def mul2_add1 (x : U32) : Result U32 :=
do
let i ← x + x
- i + 1u32
+ i + 1#u32
/- [demo::use_mul2_add1]:
Source: 'tests/src/demo.rs', lines 19:0-19:43 -/
@@ -34,13 +34,13 @@ def use_mul2_add1 (x : U32) (y : U32) : Result U32 :=
/- [demo::incr]:
Source: 'tests/src/demo.rs', lines 23:0-23:31 -/
def incr (x : U32) : Result U32 :=
- x + 1u32
+ x + 1#u32
/- [demo::use_incr]:
Source: 'tests/src/demo.rs', lines 27:0-27:17 -/
def use_incr : Result Unit :=
do
- let x ← incr 0u32
+ let x ← incr 0#u32
let x1 ← incr x
let _ ← incr x1
Result.ok ()
@@ -56,10 +56,10 @@ inductive CList (T : Type) :=
divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T :=
match l with
| CList.CCons x tl =>
- if i = 0u32
+ if i = 0#u32
then Result.ok x
else do
- let i1 ← i - 1u32
+ let i1 ← i - 1#u32
list_nth T tl i1
| CList.CNil => Result.fail .panic
@@ -71,13 +71,13 @@ divergent def list_nth_mut
:=
match l with
| CList.CCons x tl =>
- if i = 0u32
+ if i = 0#u32
then
let back := fun ret => Result.ok (CList.CCons ret tl)
Result.ok (x, back)
else
do
- let i1 ← i - 1u32
+ let i1 ← i - 1#u32
let (t, list_nth_mut_back) ← list_nth_mut T tl i1
let back :=
fun ret =>
@@ -95,13 +95,13 @@ divergent def list_nth_mut1_loop
:=
match l with
| CList.CCons x tl =>
- if i = 0u32
+ if i = 0#u32
then
let back := fun ret => Result.ok (CList.CCons ret tl)
Result.ok (x, back)
else
do
- let i1 ← i - 1u32
+ let i1 ← i - 1#u32
let (t, back) ← list_nth_mut1_loop T tl i1
let back1 :=
fun ret => do
@@ -121,12 +121,12 @@ def list_nth_mut1
/- [demo::i32_id]:
Source: 'tests/src/demo.rs', lines 82:0-82:28 -/
divergent def i32_id (i : I32) : Result I32 :=
- if i = 0i32
- then Result.ok 0i32
+ if i = 0#i32
+ then Result.ok 0#i32
else do
- let i1 ← i - 1i32
+ let i1 ← i - 1#i32
let i2 ← i32_id i1
- i2 + 1i32
+ i2 + 1#i32
/- [demo::list_tail]:
Source: 'tests/src/demo.rs', lines 90:0-90:64 -/
@@ -155,7 +155,7 @@ structure Counter (Self : Type) where
Source: 'tests/src/demo.rs', lines 104:4-104:31 -/
def CounterUsize.incr (self : Usize) : Result (Usize × Usize) :=
do
- let self1 ← self + 1usize
+ let self1 ← self + 1#usize
Result.ok (self, self1)
/- Trait implementation: [demo::{(demo::Counter for usize)}]
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index c828720a..1b1d5cdf 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -27,7 +27,7 @@ def incr
:=
do
let (st1, (i, get_mut_back)) ← core.cell.Cell.get_mut U32 rc st
- let i1 ← i + 1u32
+ let i1 ← i + 1#u32
let (_, rc1) ← get_mut_back i1 st1
Result.ok (st1, rc1)
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 3c244ee0..612e1848 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -18,11 +18,11 @@ divergent def HashMap.allocate_slots_loop
(T : Type) (slots : alloc.vec.Vec (List T)) (n : Usize) :
Result (alloc.vec.Vec (List T))
:=
- if n > 0usize
+ if n > 0#usize
then
do
let slots1 ← alloc.vec.Vec.push (List T) slots List.Nil
- let n1 ← n - 1usize
+ let n1 ← n - 1#usize
HashMap.allocate_slots_loop T slots1 n1
else Result.ok slots
@@ -47,7 +47,7 @@ def HashMap.new_with_capacity
let i1 ← i / max_load_divisor
Result.ok
{
- num_entries := 0usize,
+ num_entries := 0#usize,
max_load_factor := (max_load_dividend, max_load_divisor),
max_load := i1,
slots := slots
@@ -56,7 +56,7 @@ def HashMap.new_with_capacity
/- [hashmap::{hashmap::HashMap<T>}::new]:
Source: 'tests/src/hashmap.rs', lines 85:4-85:24 -/
def HashMap.new (T : Type) : Result (HashMap T) :=
- HashMap.new_with_capacity T 32usize 4usize 5usize
+ HashMap.new_with_capacity T 32#usize 4#usize 5#usize
/- [hashmap::{hashmap::HashMap<T>}::clear]: loop 0:
Source: 'tests/src/hashmap.rs', lines 90:4-98:5 -/
@@ -71,7 +71,7 @@ divergent def HashMap.clear_loop
let (_, index_mut_back) ←
alloc.vec.Vec.index_mut (List T) Usize
(core.slice.index.SliceIndexUsizeSliceTInst (List T)) slots i
- let i2 ← i + 1usize
+ let i2 ← i + 1#usize
let slots1 ← index_mut_back List.Nil
HashMap.clear_loop T slots1 i2
else Result.ok slots
@@ -80,8 +80,8 @@ divergent def HashMap.clear_loop
Source: 'tests/src/hashmap.rs', lines 90:4-90:27 -/
def HashMap.clear (T : Type) (self : HashMap T) : Result (HashMap T) :=
do
- let hm ← HashMap.clear_loop T self.slots 0usize
- Result.ok { self with num_entries := 0usize, slots := hm }
+ 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: 'tests/src/hashmap.rs', lines 100:4-100:30 -/
@@ -129,7 +129,7 @@ def HashMap.insert_no_resize
if inserted
then
do
- let i1 ← self.num_entries + 1usize
+ let i1 ← self.num_entries + 1#usize
let v ← index_mut_back l1
Result.ok { self with num_entries := i1, slots := v }
else do
@@ -169,7 +169,7 @@ divergent def HashMap.move_elements_loop
(core.slice.index.SliceIndexUsizeSliceTInst (List T)) slots i
let (ls, l1) := core.mem.replace (List T) l List.Nil
let ntable1 ← HashMap.move_elements_from_list T ntable ls
- let i2 ← i + 1usize
+ let i2 ← i + 1#usize
let slots1 ← index_mut_back l1
HashMap.move_elements_loop T ntable1 slots1 i2
else Result.ok (ntable, slots)
@@ -189,15 +189,15 @@ def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) :=
do
let max_usize ← Scalar.cast .Usize core_u32_max
let capacity := alloc.vec.Vec.len (List T) self.slots
- let n1 ← max_usize / 2usize
+ let n1 ← max_usize / 2#usize
let (i, i1) := self.max_load_factor
let i2 ← n1 / i
if capacity <= i2
then
do
- let i3 ← capacity * 2usize
+ let i3 ← capacity * 2#usize
let ntable ← HashMap.new_with_capacity T i3 i i1
- let p ← HashMap.move_elements T ntable self.slots 0usize
+ let p ← HashMap.move_elements T ntable self.slots 0#usize
let (ntable1, _) := p
Result.ok
{
@@ -377,7 +377,7 @@ def HashMap.remove
Result.ok (none, { self with slots := v })
| some x1 =>
do
- let i1 ← self.num_entries - 1usize
+ let i1 ← self.num_entries - 1#usize
let v ← index_mut_back l1
Result.ok (some x1, { self with num_entries := i1, slots := v })
@@ -395,37 +395,37 @@ def insert_on_disk
def test1 : Result Unit :=
do
let hm ← HashMap.new U64
- let hm1 ← HashMap.insert U64 hm 0usize 42u64
- let hm2 ← HashMap.insert U64 hm1 128usize 18u64
- let hm3 ← HashMap.insert U64 hm2 1024usize 138u64
- let hm4 ← HashMap.insert U64 hm3 1056usize 256u64
- let i ← HashMap.get U64 hm4 128usize
- if i = 18u64
+ let hm1 ← HashMap.insert U64 hm 0#usize 42#u64
+ let hm2 ← HashMap.insert U64 hm1 128#usize 18#u64
+ let hm3 ← HashMap.insert U64 hm2 1024#usize 138#u64
+ let hm4 ← HashMap.insert U64 hm3 1056#usize 256#u64
+ let i ← HashMap.get U64 hm4 128#usize
+ if i = 18#u64
then
do
- let (_, get_mut_back) ← HashMap.get_mut U64 hm4 1024usize
- let hm5 ← get_mut_back 56u64
- let i1 ← HashMap.get U64 hm5 1024usize
- if i1 = 56u64
+ let (_, get_mut_back) ← HashMap.get_mut U64 hm4 1024#usize
+ let hm5 ← get_mut_back 56#u64
+ let i1 ← HashMap.get U64 hm5 1024#usize
+ if i1 = 56#u64
then
do
- let (x, hm6) ← HashMap.remove U64 hm5 1024usize
+ let (x, hm6) ← HashMap.remove U64 hm5 1024#usize
match x with
| none => Result.fail .panic
| some x1 =>
- if x1 = 56u64
+ if x1 = 56#u64
then
do
- let i2 ← HashMap.get U64 hm6 0usize
- if i2 = 42u64
+ let i2 ← HashMap.get U64 hm6 0#usize
+ if i2 = 42#u64
then
do
- let i3 ← HashMap.get U64 hm6 128usize
- if i3 = 18u64
+ let i3 ← HashMap.get U64 hm6 128#usize
+ if i3 = 18#u64
then
do
- let i4 ← HashMap.get U64 hm6 1056usize
- if i4 = 256u64
+ let i4 ← HashMap.get U64 hm6 1056#usize
+ if i4 = 256#u64
then Result.ok ()
else Result.fail .panic
else Result.fail .panic
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index 567d2b44..199605d5 100644
--- a/tests/lean/Loops.lean
+++ b/tests/lean/Loops.lean
@@ -11,14 +11,14 @@ divergent def sum_loop (max : U32) (i : U32) (s : U32) : Result U32 :=
if i < max
then do
let s1 ← s + i
- let i1 ← i + 1u32
+ let i1 ← i + 1#u32
sum_loop max i1 s1
- else s * 2u32
+ else s * 2#u32
/- [loops::sum]:
Source: 'tests/src/loops.rs', lines 8:0-8:27 -/
def sum (max : U32) : Result U32 :=
- sum_loop max 0u32 0u32
+ sum_loop max 0#u32 0#u32
/- [loops::sum_with_mut_borrows]: loop 0:
Source: 'tests/src/loops.rs', lines 23:0-35:1 -/
@@ -28,14 +28,14 @@ divergent def sum_with_mut_borrows_loop
then
do
let ms ← s + i
- let mi ← i + 1u32
+ let mi ← i + 1#u32
sum_with_mut_borrows_loop max mi ms
- else s * 2u32
+ else s * 2#u32
/- [loops::sum_with_mut_borrows]:
Source: 'tests/src/loops.rs', lines 23:0-23:44 -/
def sum_with_mut_borrows (max : U32) : Result U32 :=
- sum_with_mut_borrows_loop max 0u32 0u32
+ sum_with_mut_borrows_loop max 0#u32 0#u32
/- [loops::sum_with_shared_borrows]: loop 0:
Source: 'tests/src/loops.rs', lines 38:0-52:1 -/
@@ -44,15 +44,15 @@ divergent def sum_with_shared_borrows_loop
if i < max
then
do
- let i1 ← i + 1u32
+ let i1 ← i + 1#u32
let s1 ← s + i1
sum_with_shared_borrows_loop max i1 s1
- else s * 2u32
+ else s * 2#u32
/- [loops::sum_with_shared_borrows]:
Source: 'tests/src/loops.rs', lines 38:0-38:47 -/
def sum_with_shared_borrows (max : U32) : Result U32 :=
- sum_with_shared_borrows_loop max 0u32 0u32
+ sum_with_shared_borrows_loop max 0#u32 0#u32
/- [loops::sum_array]: loop 0:
Source: 'tests/src/loops.rs', lines 54:0-62:1 -/
@@ -63,14 +63,14 @@ divergent def sum_array_loop
do
let i1 ← Array.index_usize U32 N a i
let s1 ← s + i1
- let i2 ← i + 1usize
+ let i2 ← i + 1#usize
sum_array_loop N a i2 s1
else Result.ok s
/- [loops::sum_array]:
Source: 'tests/src/loops.rs', lines 54:0-54:52 -/
def sum_array (N : Usize) (a : Array U32 N) : Result U32 :=
- sum_array_loop N a 0usize 0u32
+ sum_array_loop N a 0#usize 0#u32
/- [loops::clear]: loop 0:
Source: 'tests/src/loops.rs', lines 66:0-72:1 -/
@@ -83,15 +83,15 @@ divergent def clear_loop
let (_, index_mut_back) ←
alloc.vec.Vec.index_mut U32 Usize
(core.slice.index.SliceIndexUsizeSliceTInst U32) v i
- let i2 ← i + 1usize
- let v1 ← index_mut_back 0u32
+ let i2 ← i + 1#usize
+ let v1 ← index_mut_back 0#u32
clear_loop v1 i2
else Result.ok v
/- [loops::clear]:
Source: 'tests/src/loops.rs', lines 66:0-66:30 -/
def clear (v : alloc.vec.Vec U32) : Result (alloc.vec.Vec U32) :=
- clear_loop v 0usize
+ clear_loop v 0#usize
/- [loops::List]
Source: 'tests/src/loops.rs', lines 74:0-74:16 -/
@@ -119,13 +119,13 @@ divergent def list_nth_mut_loop_loop
(T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) :=
match ls with
| List.Cons x tl =>
- if i = 0u32
+ if i = 0#u32
then
let back := fun ret => Result.ok (List.Cons ret tl)
Result.ok (x, back)
else
do
- let i1 ← i - 1u32
+ let i1 ← i - 1#u32
let (t, back) ← list_nth_mut_loop_loop T tl i1
let back1 :=
fun ret => do
@@ -146,10 +146,10 @@ divergent def list_nth_shared_loop_loop
(T : Type) (ls : List T) (i : U32) : Result T :=
match ls with
| List.Cons x tl =>
- if i = 0u32
+ if i = 0#u32
then Result.ok x
else do
- let i1 ← i - 1u32
+ let i1 ← i - 1#u32
list_nth_shared_loop_loop T tl i1
| List.Nil => Result.fail .panic
@@ -189,7 +189,7 @@ def get_elem_mut
do
let (ls, index_mut_back) ←
alloc.vec.Vec.index_mut (List Usize) Usize
- (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0usize
+ (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize
let (i, back) ← get_elem_mut_loop x ls
let back1 := fun ret => do
let l ← back ret
@@ -213,7 +213,7 @@ def get_elem_shared
do
let ls ←
alloc.vec.Vec.index (List Usize) Usize
- (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0usize
+ (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize
get_elem_shared_loop x ls
/- [loops::id_mut]:
@@ -235,13 +235,13 @@ 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
| List.Cons x tl =>
- if i = 0u32
+ if i = 0#u32
then
let back := fun ret => Result.ok (List.Cons ret tl)
Result.ok (x, back)
else
do
- let i1 ← i - 1u32
+ let i1 ← i - 1#u32
let (t, back) ← list_nth_mut_loop_with_id_loop T i1 tl
let back1 :=
fun ret => do
@@ -268,10 +268,10 @@ divergent def list_nth_shared_loop_with_id_loop
(T : Type) (i : U32) (ls : List T) : Result T :=
match ls with
| List.Cons x tl =>
- if i = 0u32
+ if i = 0#u32
then Result.ok x
else do
- let i1 ← i - 1u32
+ let i1 ← i - 1#u32
list_nth_shared_loop_with_id_loop T i1 tl
| List.Nil => Result.fail .panic
@@ -293,14 +293,14 @@ divergent def list_nth_mut_loop_pair_loop
| List.Cons x0 tl0 =>
match ls1 with
| List.Cons x1 tl1 =>
- if i = 0u32
+ if i = 0#u32
then
let back'a := fun ret => Result.ok (List.Cons ret tl0)
let back'b := fun ret => Result.ok (List.Cons ret tl1)
Result.ok ((x0, x1), back'a, back'b)
else
do
- let i1 ← i - 1u32
+ let i1 ← i - 1#u32
let (p, back'a, back'b) ← list_nth_mut_loop_pair_loop T tl0 tl1 i1
let back'a1 :=
fun ret => do
@@ -330,10 +330,10 @@ divergent def list_nth_shared_loop_pair_loop
| List.Cons x0 tl0 =>
match ls1 with
| List.Cons x1 tl1 =>
- if i = 0u32
+ if i = 0#u32
then Result.ok (x0, x1)
else do
- let i1 ← i - 1u32
+ let i1 ← i - 1#u32
list_nth_shared_loop_pair_loop T tl0 tl1 i1
| List.Nil => Result.fail .panic
| List.Nil => Result.fail .panic
@@ -354,7 +354,7 @@ divergent def list_nth_mut_loop_pair_merge_loop
| List.Cons x0 tl0 =>
match ls1 with
| List.Cons x1 tl1 =>
- if i = 0u32
+ if i = 0#u32
then
let back :=
fun ret =>
@@ -363,7 +363,7 @@ divergent def list_nth_mut_loop_pair_merge_loop
Result.ok ((x0, x1), back)
else
do
- let i1 ← i - 1u32
+ let i1 ← i - 1#u32
let (p, back) ← list_nth_mut_loop_pair_merge_loop T tl0 tl1 i1
let back1 :=
fun ret =>
@@ -390,11 +390,11 @@ divergent def list_nth_shared_loop_pair_merge_loop
| List.Cons x0 tl0 =>
match ls1 with
| List.Cons x1 tl1 =>
- if i = 0u32
+ if i = 0#u32
then Result.ok (x0, x1)
else
do
- let i1 ← i - 1u32
+ let i1 ← i - 1#u32
list_nth_shared_loop_pair_merge_loop T tl0 tl1 i1
| List.Nil => Result.fail .panic
| List.Nil => Result.fail .panic
@@ -415,13 +415,13 @@ divergent def list_nth_mut_shared_loop_pair_loop
| List.Cons x0 tl0 =>
match ls1 with
| List.Cons x1 tl1 =>
- if i = 0u32
+ if i = 0#u32
then
let back := fun ret => Result.ok (List.Cons ret tl0)
Result.ok ((x0, x1), back)
else
do
- let i1 ← i - 1u32
+ let i1 ← i - 1#u32
let (p, back) ← list_nth_mut_shared_loop_pair_loop T tl0 tl1 i1
let back1 :=
fun ret => do
@@ -449,13 +449,13 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop
| List.Cons x0 tl0 =>
match ls1 with
| List.Cons x1 tl1 =>
- if i = 0u32
+ if i = 0#u32
then
let back := fun ret => Result.ok (List.Cons ret tl0)
Result.ok ((x0, x1), back)
else
do
- let i1 ← i - 1u32
+ let i1 ← i - 1#u32
let (p, back) ← list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i1
let back1 :=
fun ret => do
@@ -483,13 +483,13 @@ divergent def list_nth_shared_mut_loop_pair_loop
| List.Cons x0 tl0 =>
match ls1 with
| List.Cons x1 tl1 =>
- if i = 0u32
+ if i = 0#u32
then
let back := fun ret => Result.ok (List.Cons ret tl1)
Result.ok ((x0, x1), back)
else
do
- let i1 ← i - 1u32
+ let i1 ← i - 1#u32
let (p, back) ← list_nth_shared_mut_loop_pair_loop T tl0 tl1 i1
let back1 :=
fun ret => do
@@ -517,13 +517,13 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop
| List.Cons x0 tl0 =>
match ls1 with
| List.Cons x1 tl1 =>
- if i = 0u32
+ if i = 0#u32
then
let back := fun ret => Result.ok (List.Cons ret tl1)
Result.ok ((x0, x1), back)
else
do
- let i1 ← i - 1u32
+ let i1 ← i - 1#u32
let (p, back) ← list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i1
let back1 :=
fun ret => do
@@ -544,9 +544,9 @@ def list_nth_shared_mut_loop_pair_merge
/- [loops::ignore_input_mut_borrow]: loop 0:
Source: 'tests/src/loops.rs', lines 349:0-353:1 -/
divergent def ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
- if i > 0u32
+ if i > 0#u32
then do
- let i1 ← i - 1u32
+ let i1 ← i - 1#u32
ignore_input_mut_borrow_loop i1
else Result.ok ()
@@ -560,9 +560,9 @@ def ignore_input_mut_borrow (_a : U32) (i : U32) : Result U32 :=
/- [loops::incr_ignore_input_mut_borrow]: loop 0:
Source: 'tests/src/loops.rs', lines 357:0-362:1 -/
divergent def incr_ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
- if i > 0u32
+ if i > 0#u32
then do
- let i1 ← i - 1u32
+ let i1 ← i - 1#u32
incr_ignore_input_mut_borrow_loop i1
else Result.ok ()
@@ -570,16 +570,16 @@ divergent def incr_ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
Source: 'tests/src/loops.rs', lines 357:0-357:60 -/
def incr_ignore_input_mut_borrow (a : U32) (i : U32) : Result U32 :=
do
- let a1 ← a + 1u32
+ let a1 ← a + 1#u32
let _ ← incr_ignore_input_mut_borrow_loop i
Result.ok a1
/- [loops::ignore_input_shared_borrow]: loop 0:
Source: 'tests/src/loops.rs', lines 366:0-370:1 -/
divergent def ignore_input_shared_borrow_loop (i : U32) : Result Unit :=
- if i > 0u32
+ if i > 0#u32
then do
- let i1 ← i - 1u32
+ let i1 ← i - 1#u32
ignore_input_shared_borrow_loop i1
else Result.ok ()
diff --git a/tests/lean/Matches.lean b/tests/lean/Matches.lean
index 34f899b1..3e3a558b 100644
--- a/tests/lean/Matches.lean
+++ b/tests/lean/Matches.lean
@@ -9,8 +9,8 @@ namespace matches
Source: 'tests/src/matches.rs', lines 4:0-4:27 -/
def match_u32 (x : U32) : Result U32 :=
match x with
- | 0u32 => Result.ok 0u32
- | 1u32 => Result.ok 1u32
- | _ => Result.ok 2u32
+ | 0#u32 => Result.ok 0#u32
+ | 1#u32 => Result.ok 1#u32
+ | _ => Result.ok 2#u32
end matches
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 01f6736c..f0438050 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -62,7 +62,7 @@ def cast_bool_to_bool (x : Bool) : Result Bool :=
Source: 'tests/src/no_nested_borrows.rs', lines 63:0-63:14 -/
def test2 : Result Unit :=
do
- let _ ← 23u32 + 44u32
+ let _ ← 23#u32 + 44#u32
Result.ok ()
/- Unit test for [no_nested_borrows::test2] -/
@@ -79,10 +79,10 @@ def get_max (x : U32) (y : U32) : Result U32 :=
Source: 'tests/src/no_nested_borrows.rs', lines 83:0-83:14 -/
def test3 : Result Unit :=
do
- let x ← get_max 4u32 3u32
- let y ← get_max 10u32 11u32
+ let x ← get_max 4#u32 3#u32
+ let y ← get_max 10#u32 11#u32
let z ← x + y
- if z = 15u32
+ if z = 15#u32
then Result.ok ()
else Result.fail .panic
@@ -93,8 +93,8 @@ def test3 : Result Unit :=
Source: 'tests/src/no_nested_borrows.rs', lines 90:0-90:18 -/
def test_neg1 : Result Unit :=
do
- let y ← -. 3i32
- if y = (-3)i32
+ let y ← -. 3#i32
+ if y = (-3)#i32
then Result.ok ()
else Result.fail .panic
@@ -104,7 +104,7 @@ def test_neg1 : Result Unit :=
/- [no_nested_borrows::refs_test1]:
Source: 'tests/src/no_nested_borrows.rs', lines 97:0-97:19 -/
def refs_test1 : Result Unit :=
- if 1i32 = 1i32
+ if 1#i32 = 1#i32
then Result.ok ()
else Result.fail .panic
@@ -114,12 +114,12 @@ def refs_test1 : Result Unit :=
/- [no_nested_borrows::refs_test2]:
Source: 'tests/src/no_nested_borrows.rs', lines 108:0-108:19 -/
def refs_test2 : Result Unit :=
- if 2i32 = 2i32
+ if 2#i32 = 2#i32
then
- if 0i32 = 0i32
+ if 0#i32 = 0#i32
then
- if 2i32 = 2i32
- then if 2i32 = 2i32
+ if 2#i32 = 2#i32
+ then if 2#i32 = 2#i32
then Result.ok ()
else Result.fail .panic
else Result.fail .panic
@@ -141,10 +141,10 @@ def test_list1 : Result Unit :=
Source: 'tests/src/no_nested_borrows.rs', lines 129:0-129:18 -/
def test_box1 : Result Unit :=
do
- let (_, deref_mut_back) ← alloc.boxed.Box.deref_mut I32 0i32
- let b ← deref_mut_back 1i32
+ let (_, deref_mut_back) ← alloc.boxed.Box.deref_mut I32 0#i32
+ let b ← deref_mut_back 1#i32
let x ← alloc.boxed.Box.deref I32 b
- if x = 1i32
+ if x = 1#i32
then Result.ok ()
else Result.fail .panic
@@ -174,8 +174,8 @@ def test_panic (b : Bool) : Result Unit :=
Source: 'tests/src/no_nested_borrows.rs', lines 160:0-160:22 -/
def test_copy_int : Result Unit :=
do
- let y ← copy_int 0i32
- if 0i32 = y
+ let y ← copy_int 0#i32
+ if 0#i32 = y
then Result.ok ()
else Result.fail .panic
@@ -193,7 +193,7 @@ def is_cons (T : Type) (l : List T) : Result Bool :=
Source: 'tests/src/no_nested_borrows.rs', lines 174:0-174:21 -/
def test_is_cons : Result Unit :=
do
- let b ← is_cons I32 (List.Cons 0i32 List.Nil)
+ let b ← is_cons I32 (List.Cons 0#i32 List.Nil)
if b
then Result.ok ()
else Result.fail .panic
@@ -212,9 +212,9 @@ def split_list (T : Type) (l : List T) : Result (T × (List T)) :=
Source: 'tests/src/no_nested_borrows.rs', lines 188:0-188:24 -/
def test_split_list : Result Unit :=
do
- let p ← split_list I32 (List.Cons 0i32 List.Nil)
+ let p ← split_list I32 (List.Cons 0#i32 List.Nil)
let (hd, _) := p
- if hd = 0i32
+ if hd = 0#i32
then Result.ok ()
else Result.fail .panic
@@ -237,14 +237,14 @@ def choose
Source: 'tests/src/no_nested_borrows.rs', lines 203:0-203:20 -/
def choose_test : Result Unit :=
do
- let (z, choose_back) ← choose I32 true 0i32 0i32
- let z1 ← z + 1i32
- if z1 = 1i32
+ let (z, choose_back) ← choose I32 true 0#i32 0#i32
+ let z1 ← z + 1#i32
+ if z1 = 1#i32
then
do
let (x, y) ← choose_back z1
- if x = 1i32
- then if y = 0i32
+ if x = 1#i32
+ then if y = 0#i32
then Result.ok ()
else Result.fail .panic
else Result.fail .panic
@@ -285,18 +285,18 @@ divergent def list_length (T : Type) (l : List T) : Result U32 :=
match l with
| List.Cons _ l1 => do
let i ← list_length T l1
- 1u32 + i
- | List.Nil => Result.ok 0u32
+ 1#u32 + i
+ | List.Nil => Result.ok 0#u32
/- [no_nested_borrows::list_nth_shared]:
Source: 'tests/src/no_nested_borrows.rs', lines 273:0-273:62 -/
divergent def list_nth_shared (T : Type) (l : List T) (i : U32) : Result T :=
match l with
| List.Cons x tl =>
- if i = 0u32
+ if i = 0#u32
then Result.ok x
else do
- let i1 ← i - 1u32
+ let i1 ← i - 1#u32
list_nth_shared T tl i1
| List.Nil => Result.fail .panic
@@ -306,13 +306,13 @@ divergent def list_nth_mut
(T : Type) (l : List T) (i : U32) : Result (T × (T → Result (List T))) :=
match l with
| List.Cons x tl =>
- if i = 0u32
+ if i = 0#u32
then
let back := fun ret => Result.ok (List.Cons ret tl)
Result.ok (x, back)
else
do
- let i1 ← i - 1u32
+ let i1 ← i - 1#u32
let (t, list_nth_mut_back) ← list_nth_mut T tl i1
let back :=
fun ret =>
@@ -340,37 +340,37 @@ def list_rev (T : Type) (l : List T) : Result (List T) :=
Source: 'tests/src/no_nested_borrows.rs', lines 324:0-324:28 -/
def test_list_functions : Result Unit :=
do
- let l := List.Cons 2i32 List.Nil
- let l1 := List.Cons 1i32 l
- let i ← list_length I32 (List.Cons 0i32 l1)
- if i = 3u32
+ let l := List.Cons 2#i32 List.Nil
+ let l1 := List.Cons 1#i32 l
+ let i ← list_length I32 (List.Cons 0#i32 l1)
+ if i = 3#u32
then
do
- let i1 ← list_nth_shared I32 (List.Cons 0i32 l1) 0u32
- if i1 = 0i32
+ let i1 ← list_nth_shared I32 (List.Cons 0#i32 l1) 0#u32
+ if i1 = 0#i32
then
do
- let i2 ← list_nth_shared I32 (List.Cons 0i32 l1) 1u32
- if i2 = 1i32
+ let i2 ← list_nth_shared I32 (List.Cons 0#i32 l1) 1#u32
+ if i2 = 1#i32
then
do
- let i3 ← list_nth_shared I32 (List.Cons 0i32 l1) 2u32
- if i3 = 2i32
+ let i3 ← list_nth_shared I32 (List.Cons 0#i32 l1) 2#u32
+ if i3 = 2#i32
then
do
let (_, list_nth_mut_back) ←
- list_nth_mut I32 (List.Cons 0i32 l1) 1u32
- let ls ← list_nth_mut_back 3i32
- let i4 ← list_nth_shared I32 ls 0u32
- if i4 = 0i32
+ list_nth_mut I32 (List.Cons 0#i32 l1) 1#u32
+ let ls ← list_nth_mut_back 3#i32
+ let i4 ← list_nth_shared I32 ls 0#u32
+ if i4 = 0#i32
then
do
- let i5 ← list_nth_shared I32 ls 1u32
- if i5 = 3i32
+ let i5 ← list_nth_shared I32 ls 1#u32
+ if i5 = 3#i32
then
do
- let i6 ← list_nth_shared I32 ls 2u32
- if i6 = 2i32
+ let i6 ← list_nth_shared I32 ls 2#u32
+ if i6 = 2#i32
then Result.ok ()
else Result.fail .panic
else Result.fail .panic
@@ -425,17 +425,17 @@ structure StructWithTuple (T1 T2 : Type) where
/- [no_nested_borrows::new_tuple1]:
Source: 'tests/src/no_nested_borrows.rs', lines 363:0-363:48 -/
def new_tuple1 : Result (StructWithTuple U32 U32) :=
- Result.ok { p := (1u32, 2u32) }
+ Result.ok { p := (1#u32, 2#u32) }
/- [no_nested_borrows::new_tuple2]:
Source: 'tests/src/no_nested_borrows.rs', lines 367:0-367:48 -/
def new_tuple2 : Result (StructWithTuple I16 I16) :=
- Result.ok { p := (1i16, 2i16) }
+ Result.ok { p := (1#i16, 2#i16) }
/- [no_nested_borrows::new_tuple3]:
Source: 'tests/src/no_nested_borrows.rs', lines 371:0-371:48 -/
def new_tuple3 : Result (StructWithTuple U64 I64) :=
- Result.ok { p := (1u64, 2i64) }
+ Result.ok { p := (1#u64, 2#i64) }
/- [no_nested_borrows::StructWithPair]
Source: 'tests/src/no_nested_borrows.rs', lines 376:0-376:33 -/
@@ -445,7 +445,7 @@ structure StructWithPair (T1 T2 : Type) where
/- [no_nested_borrows::new_pair1]:
Source: 'tests/src/no_nested_borrows.rs', lines 380:0-380:46 -/
def new_pair1 : Result (StructWithPair U32 U32) :=
- Result.ok { p := { x := 1u32, y := 2u32 } }
+ Result.ok { p := { x := 1#u32, y := 2#u32 } }
/- [no_nested_borrows::test_constants]:
Source: 'tests/src/no_nested_borrows.rs', lines 388:0-388:23 -/
@@ -453,21 +453,21 @@ def test_constants : Result Unit :=
do
let swt ← new_tuple1
let (i, _) := swt.p
- if i = 1u32
+ if i = 1#u32
then
do
let swt1 ← new_tuple2
let (i1, _) := swt1.p
- if i1 = 1i16
+ if i1 = 1#i16
then
do
let swt2 ← new_tuple3
let (i2, _) := swt2.p
- if i2 = 1u64
+ if i2 = 1#u64
then
do
let swp ← new_pair1
- if swp.p.x = 1u32
+ if swp.p.x = 1#u32
then Result.ok ()
else Result.fail .panic
else Result.fail .panic
@@ -488,39 +488,39 @@ def test_weird_borrows1 : Result Unit :=
/- [no_nested_borrows::test_mem_replace]:
Source: 'tests/src/no_nested_borrows.rs', lines 407:0-407:37 -/
def test_mem_replace (px : U32) : Result U32 :=
- let (y, _) := core.mem.replace U32 px 1u32
- if y = 0u32
- then Result.ok 2u32
+ let (y, _) := core.mem.replace U32 px 1#u32
+ if y = 0#u32
+ then Result.ok 2#u32
else Result.fail .panic
/- [no_nested_borrows::test_shared_borrow_bool1]:
Source: 'tests/src/no_nested_borrows.rs', lines 414:0-414:47 -/
def test_shared_borrow_bool1 (b : Bool) : Result U32 :=
if b
- then Result.ok 0u32
- else Result.ok 1u32
+ then Result.ok 0#u32
+ else Result.ok 1#u32
/- [no_nested_borrows::test_shared_borrow_bool2]:
Source: 'tests/src/no_nested_borrows.rs', lines 427:0-427:40 -/
def test_shared_borrow_bool2 : Result U32 :=
- Result.ok 0u32
+ Result.ok 0#u32
/- [no_nested_borrows::test_shared_borrow_enum1]:
Source: 'tests/src/no_nested_borrows.rs', lines 442:0-442:52 -/
def test_shared_borrow_enum1 (l : List U32) : Result U32 :=
match l with
- | List.Cons _ _ => Result.ok 1u32
- | List.Nil => Result.ok 0u32
+ | List.Cons _ _ => Result.ok 1#u32
+ | List.Nil => Result.ok 0#u32
/- [no_nested_borrows::test_shared_borrow_enum2]:
Source: 'tests/src/no_nested_borrows.rs', lines 454:0-454:40 -/
def test_shared_borrow_enum2 : Result U32 :=
- Result.ok 0u32
+ Result.ok 0#u32
/- [no_nested_borrows::incr]:
Source: 'tests/src/no_nested_borrows.rs', lines 465:0-465:24 -/
def incr (x : U32) : Result U32 :=
- x + 1u32
+ x + 1#u32
/- [no_nested_borrows::call_incr]:
Source: 'tests/src/no_nested_borrows.rs', lines 469:0-469:35 -/
@@ -531,7 +531,7 @@ def call_incr (x : U32) : Result U32 :=
Source: 'tests/src/no_nested_borrows.rs', lines 474:0-474:41 -/
def read_then_incr (x : U32) : Result (U32 × U32) :=
do
- let x1 ← x + 1u32
+ let x1 ← x + 1#u32
Result.ok (x, x1)
/- [no_nested_borrows::Tuple]
@@ -548,7 +548,7 @@ def read_tuple (x : (U32 × U32)) : Result U32 :=
Source: 'tests/src/no_nested_borrows.rs', lines 486:0-486:39 -/
def update_tuple (x : (U32 × U32)) : Result (U32 × U32) :=
let (_, i) := x
- Result.ok (1u32, i)
+ Result.ok (1#u32, i)
/- [no_nested_borrows::read_tuple_struct]:
Source: 'tests/src/no_nested_borrows.rs', lines 490:0-490:52 -/
@@ -560,7 +560,7 @@ def read_tuple_struct (x : Tuple U32 U32) : Result U32 :=
Source: 'tests/src/no_nested_borrows.rs', lines 494:0-494:51 -/
def update_tuple_struct (x : Tuple U32 U32) : Result (Tuple U32 U32) :=
let (_, i) := x
- Result.ok (1u32, i)
+ Result.ok (1#u32, i)
/- [no_nested_borrows::create_tuple_struct]:
Source: 'tests/src/no_nested_borrows.rs', lines 498:0-498:61 -/
diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
index 400406f1..03b96903 100644
--- a/tests/lean/Paper.lean
+++ b/tests/lean/Paper.lean
@@ -8,14 +8,14 @@ namespace paper
/- [paper::ref_incr]:
Source: 'tests/src/paper.rs', lines 7:0-7:28 -/
def ref_incr (x : I32) : Result I32 :=
- x + 1i32
+ x + 1#i32
/- [paper::test_incr]:
Source: 'tests/src/paper.rs', lines 11:0-11:18 -/
def test_incr : Result Unit :=
do
- let x ← ref_incr 0i32
- if x = 1i32
+ let x ← ref_incr 0#i32
+ if x = 1#i32
then Result.ok ()
else Result.fail .panic
@@ -38,14 +38,14 @@ def choose
Source: 'tests/src/paper.rs', lines 26:0-26:20 -/
def test_choose : Result Unit :=
do
- let (z, choose_back) ← choose I32 true 0i32 0i32
- let z1 ← z + 1i32
- if z1 = 1i32
+ let (z, choose_back) ← choose I32 true 0#i32 0#i32
+ let z1 ← z + 1#i32
+ if z1 = 1#i32
then
do
let (x, y) ← choose_back z1
- if x = 1i32
- then if y = 0i32
+ if x = 1#i32
+ then if y = 0#i32
then Result.ok ()
else Result.fail .panic
else Result.fail .panic
@@ -66,13 +66,13 @@ divergent def list_nth_mut
(T : Type) (l : List T) (i : U32) : Result (T × (T → Result (List T))) :=
match l with
| List.Cons x tl =>
- if i = 0u32
+ if i = 0#u32
then
let back := fun ret => Result.ok (List.Cons ret tl)
Result.ok (x, back)
else
do
- let i1 ← i - 1u32
+ let i1 ← i - 1#u32
let (t, list_nth_mut_back) ← list_nth_mut T tl i1
let back :=
fun ret =>
@@ -89,19 +89,19 @@ divergent def sum (l : List I32) : Result I32 :=
| List.Cons x tl => do
let i ← sum tl
x + i
- | List.Nil => Result.ok 0i32
+ | List.Nil => Result.ok 0#i32
/- [paper::test_nth]:
Source: 'tests/src/paper.rs', lines 71:0-71:17 -/
def test_nth : Result Unit :=
do
- let l := List.Cons 3i32 List.Nil
- let l1 := List.Cons 2i32 l
- let (x, list_nth_mut_back) ← list_nth_mut I32 (List.Cons 1i32 l1) 2u32
- let x1 ← x + 1i32
+ let l := List.Cons 3#i32 List.Nil
+ let l1 := List.Cons 2#i32 l
+ let (x, list_nth_mut_back) ← list_nth_mut I32 (List.Cons 1#i32 l1) 2#u32
+ let x1 ← x + 1#i32
let l2 ← list_nth_mut_back x1
let i ← sum l2
- if i = 7i32
+ if i = 7#i32
then Result.ok ()
else Result.fail .panic
@@ -114,7 +114,7 @@ def call_choose (p : (U32 × U32)) : Result U32 :=
do
let (px, py) := p
let (pz, choose_back) ← choose U32 true px py
- let pz1 ← pz + 1u32
+ let pz1 ← pz + 1#u32
let (px1, _) ← choose_back pz1
Result.ok px1
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
index 1cd8644b..0dd692fe 100644
--- a/tests/lean/Traits.lean
+++ b/tests/lean/Traits.lean
@@ -148,7 +148,7 @@ structure ToType (Self T : Type) where
/- [traits::{(traits::ToType<bool> for u64)#5}::to_type]:
Source: 'tests/src/traits.rs', lines 94:4-94:28 -/
def ToTypeU64Bool.to_type (self : U64) : Result Bool :=
- Result.ok (self > 0u64)
+ Result.ok (self > 0#u64)
/- Trait implementation: [traits::{(traits::ToType<bool> for u64)#5}]
Source: 'tests/src/traits.rs', lines 93:0-93:25 -/
@@ -202,7 +202,7 @@ structure TestType.test.TestTrait (Self : Type) where
Source: 'tests/src/traits.rs', lines 140:12-140:34 -/
def TestType.test.TestTraittraitsTestTypetestTestType1.test
(self : TestType.test.TestType1) : Result Bool :=
- Result.ok (self > 1u64)
+ 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: 'tests/src/traits.rs', lines 139:8-139:36 -/
@@ -217,8 +217,8 @@ def TestType.test
(T : Type) (ToU64Inst : ToU64 T) (self : TestType T) (x : T) : Result Bool :=
do
let x1 ← ToU64Inst.to_u64 x
- if x1 > 0u64
- then TestType.test.TestTraittraitsTestTypetestTestType1.test 0u64
+ if x1 > 0#u64
+ then TestType.test.TestTraittraitsTestTypetestTestType1.test 0#u64
else Result.ok false
/- [traits::BoolWrapper]
@@ -243,7 +243,7 @@ def ToTypetraitsBoolWrapperT (T : Type) (ToTypeBoolTInst : ToType Bool T) :
/- [traits::WithConstTy::LEN2]
Source: 'tests/src/traits.rs', lines 165:4-165:21 -/
def WithConstTy.LEN2_default_body (Self : Type) (LEN : Usize) : Result Usize :=
- Result.ok 32usize
+ Result.ok 32#usize
def WithConstTy.LEN2_default (Self : Type) (LEN : Usize) : Usize :=
eval_global (WithConstTy.LEN2_default_body Self LEN)
@@ -259,19 +259,19 @@ structure WithConstTy (Self : Type) (LEN : Usize) where
/- [traits::{(traits::WithConstTy<32: usize> for bool)#8}::LEN1]
Source: 'tests/src/traits.rs', lines 176:4-176:21 -/
-def WithConstTyBool32.LEN1_body : Result Usize := Result.ok 12usize
+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: 'tests/src/traits.rs', lines 181:4-181:39 -/
-def WithConstTyBool32.f (i : U64) (a : Array U8 32usize) : Result U64 :=
+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: 'tests/src/traits.rs', lines 175:0-175:29 -/
-def WithConstTyBool32 : WithConstTy Bool 32usize := {
+def WithConstTyBool32 : WithConstTy Bool 32#usize := {
LEN1 := WithConstTyBool32.LEN1
- LEN2 := WithConstTy.LEN2_default Bool 32usize
+ LEN2 := WithConstTy.LEN2_default Bool 32#usize
V := U8
W := U64
W_clause_0 := ToU64U64
@@ -312,7 +312,7 @@ def test_where1 (T : Type) (_x : T) : Result Unit :=
/- [traits::test_where2]:
Source: 'tests/src/traits.rs', lines 195:0-195:57 -/
def test_where2
- (T : Type) (WithConstTyT32Inst : WithConstTy T 32usize) (_x : U32) :
+ (T : Type) (WithConstTyT32Inst : WithConstTy T 32#usize) (_x : U32) :
Result Unit
:=
Result.ok ()
@@ -489,7 +489,7 @@ def TraitArray (T : Type) (N : Usize) : Trait (Array T N) := {
Source: 'tests/src/traits.rs', lines 320:4-320:20 -/
def TraittraitsWrapper.LEN_body (T : Type) (TraitInst : Trait T)
: Result Usize :=
- Result.ok 0usize
+ Result.ok 0#usize
def TraittraitsWrapper.LEN (T : Type) (TraitInst : Trait T) : Usize :=
eval_global (TraittraitsWrapper.LEN_body T TraitInst)
@@ -522,7 +522,7 @@ inductive core.result.Result (T E : Type) :=
Source: 'tests/src/traits.rs', lines 333:4-333:33 -/
def Foo.FOO_body (T U : Type) (TraitInst : Trait T)
: Result (core.result.Result T I32) :=
- Result.ok (core.result.Result.Err 0i32)
+ Result.ok (core.result.Result.Err 0#i32)
def Foo.FOO (T U : Type) (TraitInst : Trait T) : core.result.Result T I32 :=
eval_global (Foo.FOO_body T U TraitInst)
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 02:37:47 +0000