summaryrefslogtreecommitdiff
path: root/tests/lean
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/lean/BetreeMain/Funs.lean31
-rw-r--r--tests/lean/Constants.lean35
-rw-r--r--tests/lean/External/Funs.lean10
-rw-r--r--tests/lean/Hashmap/Funs.lean81
-rw-r--r--tests/lean/HashmapMain/Funs.lean86
-rw-r--r--tests/lean/Loops/Funs.lean140
-rw-r--r--tests/lean/NoNestedBorrows.lean152
-rw-r--r--tests/lean/Paper.lean48
-rw-r--r--tests/lean/lake-manifest.json8
9 files changed, 269 insertions, 322 deletions
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index b0939155..142adf08 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -39,33 +39,33 @@ def betree.store_leaf_node
/- [betree_main::betree::fresh_node_id]: forward function -/
def betree.fresh_node_id (counter : U64) : Result U64 :=
do
- let _ ← counter + (U64.ofInt 1 (by intlit))
+ let _ ← counter + (U64.ofInt 1)
Result.ret counter
/- [betree_main::betree::fresh_node_id]: backward function 0 -/
def betree.fresh_node_id_back (counter : U64) : Result U64 :=
- counter + (U64.ofInt 1 (by intlit))
+ counter + (U64.ofInt 1)
/- [betree_main::betree::NodeIdCounter::{0}::new]: forward function -/
def betree.NodeIdCounter.new : Result betree.NodeIdCounter :=
- Result.ret { next_node_id := (U64.ofInt 0 (by intlit)) }
+ Result.ret { next_node_id := (U64.ofInt 0) }
/- [betree_main::betree::NodeIdCounter::{0}::fresh_id]: forward function -/
def betree.NodeIdCounter.fresh_id (self : betree.NodeIdCounter) : Result U64 :=
do
- let _ ← self.next_node_id + (U64.ofInt 1 (by intlit))
+ let _ ← self.next_node_id + (U64.ofInt 1)
Result.ret self.next_node_id
/- [betree_main::betree::NodeIdCounter::{0}::fresh_id]: backward function 0 -/
def betree.NodeIdCounter.fresh_id_back
(self : betree.NodeIdCounter) : Result betree.NodeIdCounter :=
do
- let i ← self.next_node_id + (U64.ofInt 1 (by intlit))
+ let i ← self.next_node_id + (U64.ofInt 1)
Result.ret { next_node_id := i }
/- [core::num::u64::{10}::MAX] -/
def core_num_u64_max_body : Result U64 :=
- Result.ret (U64.ofInt 18446744073709551615 (by intlit))
+ Result.ret (U64.ofInt 18446744073709551615)
def core_num_u64_max_c : U64 := eval_global core_num_u64_max_body (by simp)
/- [betree_main::betree::upsert_update]: forward function -/
@@ -75,7 +75,7 @@ def betree.upsert_update
| Option.none =>
match st with
| betree.UpsertFunState.Add v => Result.ret v
- | betree.UpsertFunState.Sub i => Result.ret (U64.ofInt 0 (by intlit))
+ | betree.UpsertFunState.Sub i => Result.ret (U64.ofInt 0)
| Option.some prev0 =>
match st with
| betree.UpsertFunState.Add v =>
@@ -87,7 +87,7 @@ def betree.upsert_update
| betree.UpsertFunState.Sub v =>
if prev0 >= v
then prev0 - v
- else Result.ret (U64.ofInt 0 (by intlit))
+ else Result.ret (U64.ofInt 0)
/- [betree_main::betree::List::{1}::len]: forward function -/
divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
@@ -95,21 +95,21 @@ divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
| betree.List.Cons t tl =>
do
let i ← betree.List.len T tl
- (U64.ofInt 1 (by intlit)) + i
- | betree.List.Nil => Result.ret (U64.ofInt 0 (by intlit))
+ (U64.ofInt 1) + i
+ | betree.List.Nil => Result.ret (U64.ofInt 0)
/- [betree_main::betree::List::{1}::split_at]: forward function -/
divergent def betree.List.split_at
(T : Type) (self : betree.List T) (n : U64) :
Result ((betree.List T) × (betree.List T))
:=
- if n = (U64.ofInt 0 (by intlit))
+ if n = (U64.ofInt 0)
then Result.ret (betree.List.Nil, self)
else
match self with
| betree.List.Cons hd tl =>
do
- let i ← n - (U64.ofInt 1 (by intlit))
+ let i ← n - (U64.ofInt 1)
let p ← betree.List.split_at T tl i
let (ls0, ls1) := p
let l := ls0
@@ -740,7 +740,7 @@ mutual divergent def betree.Node.apply_messages
let (st0, content) ← betree.load_leaf_node node.id st
let content0 ← betree.Node.apply_messages_to_leaf content msgs
let len ← betree.List.len (U64 × U64) content0
- let i ← (U64.ofInt 2 (by intlit)) * params.split_size
+ let i ← (U64.ofInt 2) * params.split_size
if len >= i
then
do
@@ -790,7 +790,7 @@ divergent def betree.Node.apply_messages_back
let (st0, content) ← betree.load_leaf_node node.id st
let content0 ← betree.Node.apply_messages_to_leaf content msgs
let len ← betree.List.len (U64 × U64) content0
- let i ← (U64.ofInt 2 (by intlit)) * params.split_size
+ let i ← (U64.ofInt 2) * params.split_size
if len >= i
then
do
@@ -922,8 +922,7 @@ def betree.BeTree.new
params :=
{ min_flush_size := min_flush_size, split_size := split_size },
node_id_cnt := node_id_cnt0,
- root :=
- (betree.Node.Leaf { id := id, size := (U64.ofInt 0 (by intlit)) })
+ root := (betree.Node.Leaf { id := id, size := (U64.ofInt 0) })
})
/- [betree_main::betree::BeTree::{6}::apply]: forward function -/
diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean
index 8f22bfba..4a5a7b8f 100644
--- a/tests/lean/Constants.lean
+++ b/tests/lean/Constants.lean
@@ -5,12 +5,11 @@ open Primitives
namespace constants
/- [constants::X0] -/
-def x0_body : Result U32 := Result.ret (U32.ofInt 0 (by intlit))
+def x0_body : Result U32 := Result.ret (U32.ofInt 0)
def x0_c : U32 := eval_global x0_body (by simp)
/- [core::num::u32::{9}::MAX] -/
-def core_num_u32_max_body : Result U32 :=
- Result.ret (U32.ofInt 4294967295 (by intlit))
+def core_num_u32_max_body : Result U32 := Result.ret (U32.ofInt 4294967295)
def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp)
/- [constants::X1] -/
@@ -18,15 +17,15 @@ def x1_body : Result U32 := Result.ret core_num_u32_max_c
def x1_c : U32 := eval_global x1_body (by simp)
/- [constants::X2] -/
-def x2_body : Result U32 := Result.ret (U32.ofInt 3 (by intlit))
+def x2_body : Result U32 := Result.ret (U32.ofInt 3)
def x2_c : U32 := eval_global x2_body (by simp)
/- [constants::incr]: forward function -/
def incr (n : U32) : Result U32 :=
- n + (U32.ofInt 1 (by intlit))
+ n + (U32.ofInt 1)
/- [constants::X3] -/
-def x3_body : Result U32 := incr (U32.ofInt 32 (by intlit))
+def x3_body : Result U32 := incr (U32.ofInt 32)
def x3_c : U32 := eval_global x3_body (by simp)
/- [constants::mk_pair0]: forward function -/
@@ -43,23 +42,20 @@ def mk_pair1 (x : U32) (y : U32) : Result (Pair U32 U32) :=
Result.ret { x := x, y := y }
/- [constants::P0] -/
-def p0_body : Result (U32 × U32) :=
- mk_pair0 (U32.ofInt 0 (by intlit)) (U32.ofInt 1 (by intlit))
+def p0_body : Result (U32 × U32) := mk_pair0 (U32.ofInt 0) (U32.ofInt 1)
def p0_c : (U32 × U32) := eval_global p0_body (by simp)
/- [constants::P1] -/
-def p1_body : Result (Pair U32 U32) :=
- mk_pair1 (U32.ofInt 0 (by intlit)) (U32.ofInt 1 (by intlit))
+def p1_body : Result (Pair U32 U32) := mk_pair1 (U32.ofInt 0) (U32.ofInt 1)
def p1_c : Pair U32 U32 := eval_global p1_body (by simp)
/- [constants::P2] -/
-def p2_body : Result (U32 × U32) :=
- Result.ret ((U32.ofInt 0 (by intlit)), (U32.ofInt 1 (by intlit)))
+def p2_body : Result (U32 × U32) := Result.ret ((U32.ofInt 0), (U32.ofInt 1))
def p2_c : (U32 × U32) := eval_global p2_body (by simp)
/- [constants::P3] -/
def p3_body : Result (Pair U32 U32) :=
- Result.ret { x := (U32.ofInt 0 (by intlit)), y := (U32.ofInt 1 (by intlit)) }
+ Result.ret { x := (U32.ofInt 0), y := (U32.ofInt 1) }
def p3_c : Pair U32 U32 := eval_global p3_body (by simp)
/- [constants::Wrap] -/
@@ -71,7 +67,7 @@ def Wrap.new (T : Type) (val : T) : Result (Wrap T) :=
Result.ret { val := val }
/- [constants::Y] -/
-def y_body : Result (Wrap I32) := Wrap.new I32 (I32.ofInt 2 (by intlit))
+def y_body : Result (Wrap I32) := Wrap.new I32 (I32.ofInt 2)
def y_c : Wrap I32 := eval_global y_body (by simp)
/- [constants::unwrap_y]: forward function -/
@@ -83,7 +79,7 @@ def yval_body : Result I32 := unwrap_y
def yval_c : I32 := eval_global yval_body (by simp)
/- [constants::get_z1::Z1] -/
-def get_z1_z1_body : Result I32 := Result.ret (I32.ofInt 3 (by intlit))
+def get_z1_z1_body : Result I32 := Result.ret (I32.ofInt 3)
def get_z1_z1_c : I32 := eval_global get_z1_z1_body (by simp)
/- [constants::get_z1]: forward function -/
@@ -95,7 +91,7 @@ def add (a : I32) (b : I32) : Result I32 :=
a + b
/- [constants::Q1] -/
-def q1_body : Result I32 := Result.ret (I32.ofInt 5 (by intlit))
+def q1_body : Result I32 := Result.ret (I32.ofInt 5)
def q1_c : I32 := eval_global q1_body (by simp)
/- [constants::Q2] -/
@@ -103,7 +99,7 @@ def q2_body : Result I32 := Result.ret q1_c
def q2_c : I32 := eval_global q2_body (by simp)
/- [constants::Q3] -/
-def q3_body : Result I32 := add q2_c (I32.ofInt 3 (by intlit))
+def q3_body : Result I32 := add q2_c (I32.ofInt 3)
def q3_c : I32 := eval_global q3_body (by simp)
/- [constants::get_z2]: forward function -/
@@ -114,7 +110,7 @@ def get_z2 : Result I32 :=
add q1_c i0
/- [constants::S1] -/
-def s1_body : Result U32 := Result.ret (U32.ofInt 6 (by intlit))
+def s1_body : Result U32 := Result.ret (U32.ofInt 6)
def s1_c : U32 := eval_global s1_body (by simp)
/- [constants::S2] -/
@@ -126,8 +122,7 @@ def s3_body : Result (Pair U32 U32) := Result.ret p3_c
def s3_c : Pair U32 U32 := eval_global s3_body (by simp)
/- [constants::S4] -/
-def s4_body : Result (Pair U32 U32) :=
- mk_pair1 (U32.ofInt 7 (by intlit)) (U32.ofInt 8 (by intlit))
+def s4_body : Result (Pair U32 U32) := mk_pair1 (U32.ofInt 7) (U32.ofInt 8)
def s4_c : Pair U32 U32 := eval_global s4_body (by simp)
end constants
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index 122f94da..674aaebd 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -36,7 +36,7 @@ def test_new_non_zero_u32
def test_vec : Result Unit :=
do
let v := Vec.new U32
- let _ ← Vec.push U32 v (U32.ofInt 0 (by intlit))
+ let _ ← Vec.push U32 v (U32.ofInt 0)
Result.ret ()
/- Unit test for [external::test_vec] -/
@@ -74,14 +74,14 @@ def test_custom_swap_back
(x : U32) (y : U32) (st : State) (st0 : State) :
Result (State × (U32 × U32))
:=
- custom_swap_back U32 x y st (U32.ofInt 1 (by intlit)) st0
+ custom_swap_back U32 x y st (U32.ofInt 1) st0
/- [external::test_swap_non_zero]: forward function -/
def test_swap_non_zero (x : U32) (st : State) : Result (State × U32) :=
do
- let (st0, _) ← swap U32 x (U32.ofInt 0 (by intlit)) st
- let (st1, (x0, _)) ← swap_back U32 x (U32.ofInt 0 (by intlit)) st st0
- if x0 = (U32.ofInt 0 (by intlit))
+ let (st0, _) ← swap U32 x (U32.ofInt 0) st
+ let (st1, (x0, _)) ← swap_back U32 x (U32.ofInt 0) st st0
+ if x0 = (U32.ofInt 0)
then Result.fail Error.panic
else Result.ret (st1, x0)
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 5e11ffdd..870693b5 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -12,11 +12,11 @@ def hash_key (k : Usize) : Result Usize :=
/- [hashmap::HashMap::{0}::allocate_slots]: loop 0: forward function -/
divergent def HashMap.allocate_slots_loop
(T : Type) (slots : Vec (List T)) (n : Usize) : Result (Vec (List T)) :=
- if n > (Usize.ofInt 0 (by intlit))
+ if n > (Usize.ofInt 0)
then
do
let slots0 ← Vec.push (List T) slots List.Nil
- let n0 ← n - (Usize.ofInt 1 (by intlit))
+ let n0 ← n - (Usize.ofInt 1)
HashMap.allocate_slots_loop T slots0 n0
else Result.ret slots
@@ -38,7 +38,7 @@ def HashMap.new_with_capacity
let i0 ← i / max_load_divisor
Result.ret
{
- num_entries := (Usize.ofInt 0 (by intlit)),
+ num_entries := (Usize.ofInt 0),
max_load_factor := (max_load_dividend, max_load_divisor),
max_load := i0,
slots := slots
@@ -46,8 +46,7 @@ def HashMap.new_with_capacity
/- [hashmap::HashMap::{0}::new]: forward function -/
def HashMap.new (T : Type) : Result (HashMap T) :=
- HashMap.new_with_capacity T (Usize.ofInt 32 (by intlit))
- (Usize.ofInt 4 (by intlit)) (Usize.ofInt 5 (by intlit))
+ HashMap.new_with_capacity T (Usize.ofInt 32) (Usize.ofInt 4) (Usize.ofInt 5)
/- [hashmap::HashMap::{0}::clear]: loop 0: merged forward/backward function
(there is a single backward function, and the forward function returns ()) -/
@@ -57,7 +56,7 @@ divergent def HashMap.clear_loop
if i < i0
then
do
- let i1 ← i + (Usize.ofInt 1 (by intlit))
+ let i1 ← i + (Usize.ofInt 1)
let slots0 ← Vec.index_mut_back (List T) slots i List.Nil
HashMap.clear_loop T slots0 i1
else Result.ret slots
@@ -66,9 +65,8 @@ divergent def HashMap.clear_loop
(there is a single backward function, and the forward function returns ()) -/
def HashMap.clear (T : Type) (self : HashMap T) : Result (HashMap T) :=
do
- let v ← HashMap.clear_loop T self.slots (Usize.ofInt 0 (by intlit))
- Result.ret
- { self with num_entries := (Usize.ofInt 0 (by intlit)), slots := v }
+ let v ← HashMap.clear_loop T self.slots (Usize.ofInt 0)
+ Result.ret { self with num_entries := (Usize.ofInt 0), slots := v }
/- [hashmap::HashMap::{0}::len]: forward function -/
def HashMap.len (T : Type) (self : HashMap T) : Result Usize :=
@@ -123,7 +121,7 @@ def HashMap.insert_no_resize
if inserted
then
do
- let i0 ← self.num_entries + (Usize.ofInt 1 (by intlit))
+ let i0 ← self.num_entries + (Usize.ofInt 1)
let l0 ← HashMap.insert_in_list_back T key value l
let v ← Vec.index_mut_back (List T) self.slots hash_mod l0
Result.ret { self with num_entries := i0, slots := v }
@@ -134,8 +132,7 @@ def HashMap.insert_no_resize
Result.ret { self with slots := v }
/- [core::num::u32::{9}::MAX] -/
-def core_num_u32_max_body : Result U32 :=
- Result.ret (U32.ofInt 4294967295 (by intlit))
+def core_num_u32_max_body : Result U32 := Result.ret (U32.ofInt 4294967295)
def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp)
/- [hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
@@ -168,7 +165,7 @@ divergent def HashMap.move_elements_loop
let l ← Vec.index_mut (List T) slots i
let ls := mem.replace (List T) l List.Nil
let ntable0 ← HashMap.move_elements_from_list T ntable ls
- let i1 ← i + (Usize.ofInt 1 (by intlit))
+ let i1 ← i + (Usize.ofInt 1)
let l0 := mem.replace_back (List T) l List.Nil
let slots0 ← Vec.index_mut_back (List T) slots i l0
HashMap.move_elements_loop T ntable0 slots0 i1
@@ -188,16 +185,16 @@ def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) :=
do
let max_usize ← Scalar.cast .Usize core_num_u32_max_c
let capacity := Vec.len (List T) self.slots
- let n1 ← max_usize / (Usize.ofInt 2 (by intlit))
+ let n1 ← max_usize / (Usize.ofInt 2)
let (i, i0) := self.max_load_factor
let i1 ← n1 / i
if capacity <= i1
then
do
- let i2 ← capacity * (Usize.ofInt 2 (by intlit))
+ let i2 ← capacity * (Usize.ofInt 2)
let ntable ← HashMap.new_with_capacity T i2 i i0
let (ntable0, _) ←
- HashMap.move_elements T ntable self.slots (Usize.ofInt 0 (by intlit))
+ HashMap.move_elements T ntable self.slots (Usize.ofInt 0)
Result.ret
{
ntable0
@@ -377,7 +374,7 @@ def HashMap.remove
| Option.none => Result.ret Option.none
| Option.some x0 =>
do
- let _ ← self.num_entries - (Usize.ofInt 1 (by intlit))
+ let _ ← self.num_entries - (Usize.ofInt 1)
Result.ret (Option.some x0)
/- [hashmap::HashMap::{0}::remove]: backward function 0 -/
@@ -397,7 +394,7 @@ def HashMap.remove_back
Result.ret { self with slots := v }
| Option.some x0 =>
do
- let i0 ← self.num_entries - (Usize.ofInt 1 (by intlit))
+ let i0 ← self.num_entries - (Usize.ofInt 1)
let l0 ← HashMap.remove_from_list_back T key l
let v ← Vec.index_mut_back (List T) self.slots hash_mod l0
Result.ret { self with num_entries := i0, slots := v }
@@ -406,55 +403,43 @@ def HashMap.remove_back
def test1 : Result Unit :=
do
let hm ← HashMap.new U64
- let hm0 ←
- HashMap.insert U64 hm (Usize.ofInt 0 (by intlit))
- (U64.ofInt 42 (by intlit))
- let hm1 ←
- HashMap.insert U64 hm0 (Usize.ofInt 128 (by intlit))
- (U64.ofInt 18 (by intlit))
- let hm2 ←
- HashMap.insert U64 hm1 (Usize.ofInt 1024 (by intlit))
- (U64.ofInt 138 (by intlit))
- let hm3 ←
- HashMap.insert U64 hm2 (Usize.ofInt 1056 (by intlit))
- (U64.ofInt 256 (by intlit))
- let i ← HashMap.get U64 hm3 (Usize.ofInt 128 (by intlit))
- if not (i = (U64.ofInt 18 (by intlit)))
+ let hm0 ← HashMap.insert U64 hm (Usize.ofInt 0) (U64.ofInt 42)
+ let hm1 ← HashMap.insert U64 hm0 (Usize.ofInt 128) (U64.ofInt 18)
+ let hm2 ← HashMap.insert U64 hm1 (Usize.ofInt 1024) (U64.ofInt 138)
+ let hm3 ← HashMap.insert U64 hm2 (Usize.ofInt 1056) (U64.ofInt 256)
+ let i ← HashMap.get U64 hm3 (Usize.ofInt 128)
+ if not (i = (U64.ofInt 18))
then Result.fail Error.panic
else
do
let hm4 ←
- HashMap.get_mut_back U64 hm3 (Usize.ofInt 1024 (by intlit))
- (U64.ofInt 56 (by intlit))
- let i0 ← HashMap.get U64 hm4 (Usize.ofInt 1024 (by intlit))
- if not (i0 = (U64.ofInt 56 (by intlit)))
+ HashMap.get_mut_back U64 hm3 (Usize.ofInt 1024) (U64.ofInt 56)
+ let i0 ← HashMap.get U64 hm4 (Usize.ofInt 1024)
+ if not (i0 = (U64.ofInt 56))
then Result.fail Error.panic
else
do
- let x ← HashMap.remove U64 hm4 (Usize.ofInt 1024 (by intlit))
+ let x ← HashMap.remove U64 hm4 (Usize.ofInt 1024)
match x with
| Option.none => Result.fail Error.panic
| Option.some x0 =>
- if not (x0 = (U64.ofInt 56 (by intlit)))
+ if not (x0 = (U64.ofInt 56))
then Result.fail Error.panic
else
do
- let hm5 ←
- HashMap.remove_back U64 hm4 (Usize.ofInt 1024 (by intlit))
- let i1 ← HashMap.get U64 hm5 (Usize.ofInt 0 (by intlit))
- if not (i1 = (U64.ofInt 42 (by intlit)))
+ let hm5 ← HashMap.remove_back U64 hm4 (Usize.ofInt 1024)
+ let i1 ← HashMap.get U64 hm5 (Usize.ofInt 0)
+ if not (i1 = (U64.ofInt 42))
then Result.fail Error.panic
else
do
- let i2 ←
- HashMap.get U64 hm5 (Usize.ofInt 128 (by intlit))
- if not (i2 = (U64.ofInt 18 (by intlit)))
+ let i2 ← HashMap.get U64 hm5 (Usize.ofInt 128)
+ if not (i2 = (U64.ofInt 18))
then Result.fail Error.panic
else
do
- let i3 ←
- HashMap.get U64 hm5 (Usize.ofInt 1056 (by intlit))
- if not (i3 = (U64.ofInt 256 (by intlit)))
+ let i3 ← HashMap.get U64 hm5 (Usize.ofInt 1056)
+ if not (i3 = (U64.ofInt 256))
then Result.fail Error.panic
else Result.ret ()
diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean
index e82cc9b2..610bae46 100644
--- a/tests/lean/HashmapMain/Funs.lean
+++ b/tests/lean/HashmapMain/Funs.lean
@@ -15,11 +15,11 @@ divergent def hashmap.HashMap.allocate_slots_loop
(T : Type) (slots : Vec (hashmap.List T)) (n : Usize) :
Result (Vec (hashmap.List T))
:=
- if n > (Usize.ofInt 0 (by intlit))
+ if n > (Usize.ofInt 0)
then
do
let slots0 ← Vec.push (hashmap.List T) slots hashmap.List.Nil
- let n0 ← n - (Usize.ofInt 1 (by intlit))
+ let n0 ← n - (Usize.ofInt 1)
hashmap.HashMap.allocate_slots_loop T slots0 n0
else Result.ret slots
@@ -43,7 +43,7 @@ def hashmap.HashMap.new_with_capacity
let i0 ← i / max_load_divisor
Result.ret
{
- num_entries := (Usize.ofInt 0 (by intlit)),
+ num_entries := (Usize.ofInt 0),
max_load_factor := (max_load_dividend, max_load_divisor),
max_load := i0,
slots := slots
@@ -51,8 +51,8 @@ def hashmap.HashMap.new_with_capacity
/- [hashmap_main::hashmap::HashMap::{0}::new]: forward function -/
def hashmap.HashMap.new (T : Type) : Result (hashmap.HashMap T) :=
- hashmap.HashMap.new_with_capacity T (Usize.ofInt 32 (by intlit))
- (Usize.ofInt 4 (by intlit)) (Usize.ofInt 5 (by intlit))
+ hashmap.HashMap.new_with_capacity T (Usize.ofInt 32) (Usize.ofInt 4)
+ (Usize.ofInt 5)
/- [hashmap_main::hashmap::HashMap::{0}::clear]: loop 0: merged forward/backward function
(there is a single backward function, and the forward function returns ()) -/
@@ -64,7 +64,7 @@ divergent def hashmap.HashMap.clear_loop
if i < i0
then
do
- let i1 ← i + (Usize.ofInt 1 (by intlit))
+ let i1 ← i + (Usize.ofInt 1)
let slots0 ←
Vec.index_mut_back (hashmap.List T) slots i hashmap.List.Nil
hashmap.HashMap.clear_loop T slots0 i1
@@ -75,10 +75,8 @@ divergent def hashmap.HashMap.clear_loop
def hashmap.HashMap.clear
(T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) :=
do
- let v ←
- hashmap.HashMap.clear_loop T self.slots (Usize.ofInt 0 (by intlit))
- Result.ret
- { self with num_entries := (Usize.ofInt 0 (by intlit)), slots := v }
+ let v ← hashmap.HashMap.clear_loop T self.slots (Usize.ofInt 0)
+ Result.ret { self with num_entries := (Usize.ofInt 0), slots := v }
/- [hashmap_main::hashmap::HashMap::{0}::len]: forward function -/
def hashmap.HashMap.len (T : Type) (self : hashmap.HashMap T) : Result Usize :=
@@ -138,7 +136,7 @@ def hashmap.HashMap.insert_no_resize
if inserted
then
do
- let i0 ← self.num_entries + (Usize.ofInt 1 (by intlit))
+ let i0 ← self.num_entries + (Usize.ofInt 1)
let l0 ← hashmap.HashMap.insert_in_list_back T key value l
let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0
Result.ret { self with num_entries := i0, slots := v }
@@ -149,8 +147,7 @@ def hashmap.HashMap.insert_no_resize
Result.ret { self with slots := v }
/- [core::num::u32::{9}::MAX] -/
-def core_num_u32_max_body : Result U32 :=
- Result.ret (U32.ofInt 4294967295 (by intlit))
+def core_num_u32_max_body : Result U32 := Result.ret (U32.ofInt 4294967295)
def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp)
/- [hashmap_main::hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
@@ -188,7 +185,7 @@ divergent def hashmap.HashMap.move_elements_loop
let l ← Vec.index_mut (hashmap.List T) slots i
let ls := mem.replace (hashmap.List T) l hashmap.List.Nil
let ntable0 ← hashmap.HashMap.move_elements_from_list T ntable ls
- let i1 ← i + (Usize.ofInt 1 (by intlit))
+ let i1 ← i + (Usize.ofInt 1)
let l0 := mem.replace_back (hashmap.List T) l hashmap.List.Nil
let slots0 ← Vec.index_mut_back (hashmap.List T) slots i l0
hashmap.HashMap.move_elements_loop T ntable0 slots0 i1
@@ -210,17 +207,16 @@ def hashmap.HashMap.try_resize
do
let max_usize ← Scalar.cast .Usize core_num_u32_max_c
let capacity := Vec.len (hashmap.List T) self.slots
- let n1 ← max_usize / (Usize.ofInt 2 (by intlit))
+ let n1 ← max_usize / (Usize.ofInt 2)
let (i, i0) := self.max_load_factor
let i1 ← n1 / i
if capacity <= i1
then
do
- let i2 ← capacity * (Usize.ofInt 2 (by intlit))
+ let i2 ← capacity * (Usize.ofInt 2)
let ntable ← hashmap.HashMap.new_with_capacity T i2 i i0
let (ntable0, _) ←
- hashmap.HashMap.move_elements T ntable self.slots
- (Usize.ofInt 0 (by intlit))
+ hashmap.HashMap.move_elements T ntable self.slots (Usize.ofInt 0)
Result.ret
{
ntable0
@@ -411,7 +407,7 @@ def hashmap.HashMap.remove
| Option.none => Result.ret Option.none
| Option.some x0 =>
do
- let _ ← self.num_entries - (Usize.ofInt 1 (by intlit))
+ let _ ← self.num_entries - (Usize.ofInt 1)
Result.ret (Option.some x0)
/- [hashmap_main::hashmap::HashMap::{0}::remove]: backward function 0 -/
@@ -433,7 +429,7 @@ def hashmap.HashMap.remove_back
Result.ret { self with slots := v }
| Option.some x0 =>
do
- let i0 ← self.num_entries - (Usize.ofInt 1 (by intlit))
+ let i0 ← self.num_entries - (Usize.ofInt 1)
let l0 ← hashmap.HashMap.remove_from_list_back T key l
let v ← Vec.index_mut_back (hashmap.List T) self.slots hash_mod l0
Result.ret { self with num_entries := i0, slots := v }
@@ -442,60 +438,48 @@ def hashmap.HashMap.remove_back
def hashmap.test1 : Result Unit :=
do
let hm ← hashmap.HashMap.new U64
- let hm0 ←
- hashmap.HashMap.insert U64 hm (Usize.ofInt 0 (by intlit))
- (U64.ofInt 42 (by intlit))
- let hm1 ←
- hashmap.HashMap.insert U64 hm0 (Usize.ofInt 128 (by intlit))
- (U64.ofInt 18 (by intlit))
+ let hm0 ← hashmap.HashMap.insert U64 hm (Usize.ofInt 0) (U64.ofInt 42)
+ let hm1 ← hashmap.HashMap.insert U64 hm0 (Usize.ofInt 128) (U64.ofInt 18)
let hm2 ←
- hashmap.HashMap.insert U64 hm1 (Usize.ofInt 1024 (by intlit))
- (U64.ofInt 138 (by intlit))
+ hashmap.HashMap.insert U64 hm1 (Usize.ofInt 1024) (U64.ofInt 138)
let hm3 ←
- hashmap.HashMap.insert U64 hm2 (Usize.ofInt 1056 (by intlit))
- (U64.ofInt 256 (by intlit))
- let i ← hashmap.HashMap.get U64 hm3 (Usize.ofInt 128 (by intlit))
- if not (i = (U64.ofInt 18 (by intlit)))
+ hashmap.HashMap.insert U64 hm2 (Usize.ofInt 1056) (U64.ofInt 256)
+ let i ← hashmap.HashMap.get U64 hm3 (Usize.ofInt 128)
+ if not (i = (U64.ofInt 18))
then Result.fail Error.panic
else
do
let hm4 ←
- hashmap.HashMap.get_mut_back U64 hm3 (Usize.ofInt 1024 (by intlit))
- (U64.ofInt 56 (by intlit))
- let i0 ← hashmap.HashMap.get U64 hm4 (Usize.ofInt 1024 (by intlit))
- if not (i0 = (U64.ofInt 56 (by intlit)))
+ hashmap.HashMap.get_mut_back U64 hm3 (Usize.ofInt 1024)
+ (U64.ofInt 56)
+ let i0 ← hashmap.HashMap.get U64 hm4 (Usize.ofInt 1024)
+ if not (i0 = (U64.ofInt 56))
then Result.fail Error.panic
else
do
- let x ←
- hashmap.HashMap.remove U64 hm4 (Usize.ofInt 1024 (by intlit))
+ let x ← hashmap.HashMap.remove U64 hm4 (Usize.ofInt 1024)
match x with
| Option.none => Result.fail Error.panic
| Option.some x0 =>
- if not (x0 = (U64.ofInt 56 (by intlit)))
+ if not (x0 = (U64.ofInt 56))
then Result.fail Error.panic
else
do
let hm5 ←
- hashmap.HashMap.remove_back U64 hm4
- (Usize.ofInt 1024 (by intlit))
- let i1 ←
- hashmap.HashMap.get U64 hm5 (Usize.ofInt 0 (by intlit))
- if not (i1 = (U64.ofInt 42 (by intlit)))
+ hashmap.HashMap.remove_back U64 hm4 (Usize.ofInt 1024)
+ let i1 ← hashmap.HashMap.get U64 hm5 (Usize.ofInt 0)
+ if not (i1 = (U64.ofInt 42))
then Result.fail Error.panic
else
do
- let i2 ←
- hashmap.HashMap.get U64 hm5
- (Usize.ofInt 128 (by intlit))
- if not (i2 = (U64.ofInt 18 (by intlit)))
+ let i2 ← hashmap.HashMap.get U64 hm5 (Usize.ofInt 128)
+ if not (i2 = (U64.ofInt 18))
then Result.fail Error.panic
else
do
let i3 ←
- hashmap.HashMap.get U64 hm5
- (Usize.ofInt 1056 (by intlit))
- if not (i3 = (U64.ofInt 256 (by intlit)))
+ hashmap.HashMap.get U64 hm5 (Usize.ofInt 1056)
+ if not (i3 = (U64.ofInt 256))
then Result.fail Error.panic
else Result.ret ()
diff --git a/tests/lean/Loops/Funs.lean b/tests/lean/Loops/Funs.lean
index 8cac7ac0..f7e6603d 100644
--- a/tests/lean/Loops/Funs.lean
+++ b/tests/lean/Loops/Funs.lean
@@ -8,16 +8,15 @@ namespace loops
/- [loops::sum]: loop 0: forward function -/
divergent def sum_loop (max : U32) (i : U32) (s : U32) : Result U32 :=
if i < max
- then
- do
- let s0 ← s + i
- let i0 ← i + (U32.ofInt 1 (by intlit))
- sum_loop max i0 s0
- else s * (U32.ofInt 2 (by intlit))
+ then do
+ let s0 ← s + i
+ let i0 ← i + (U32.ofInt 1)
+ sum_loop max i0 s0
+ else s * (U32.ofInt 2)
/- [loops::sum]: forward function -/
def sum (max : U32) : Result U32 :=
- sum_loop max (U32.ofInt 0 (by intlit)) (U32.ofInt 0 (by intlit))
+ sum_loop max (U32.ofInt 0) (U32.ofInt 0)
/- [loops::sum_with_mut_borrows]: loop 0: forward function -/
divergent def sum_with_mut_borrows_loop
@@ -26,14 +25,13 @@ divergent def sum_with_mut_borrows_loop
then
do
let ms0 ← ms + mi
- let mi0 ← mi + (U32.ofInt 1 (by intlit))
+ let mi0 ← mi + (U32.ofInt 1)
sum_with_mut_borrows_loop max mi0 ms0
- else ms * (U32.ofInt 2 (by intlit))
+ else ms * (U32.ofInt 2)
/- [loops::sum_with_mut_borrows]: forward function -/
def sum_with_mut_borrows (max : U32) : Result U32 :=
- sum_with_mut_borrows_loop max (U32.ofInt 0 (by intlit))
- (U32.ofInt 0 (by intlit))
+ sum_with_mut_borrows_loop max (U32.ofInt 0) (U32.ofInt 0)
/- [loops::sum_with_shared_borrows]: loop 0: forward function -/
divergent def sum_with_shared_borrows_loop
@@ -41,15 +39,14 @@ divergent def sum_with_shared_borrows_loop
if i < max
then
do
- let i0 ← i + (U32.ofInt 1 (by intlit))
+ let i0 ← i + (U32.ofInt 1)
let s0 ← s + i0
sum_with_shared_borrows_loop max i0 s0
- else s * (U32.ofInt 2 (by intlit))
+ else s * (U32.ofInt 2)
/- [loops::sum_with_shared_borrows]: forward function -/
def sum_with_shared_borrows (max : U32) : Result U32 :=
- sum_with_shared_borrows_loop max (U32.ofInt 0 (by intlit))
- (U32.ofInt 0 (by intlit))
+ sum_with_shared_borrows_loop max (U32.ofInt 0) (U32.ofInt 0)
/- [loops::clear]: loop 0: merged forward/backward function
(there is a single backward function, and the forward function returns ()) -/
@@ -58,15 +55,15 @@ divergent def clear_loop (v : Vec U32) (i : Usize) : Result (Vec U32) :=
if i < i0
then
do
- let i1 ← i + (Usize.ofInt 1 (by intlit))
- let v0 ← Vec.index_mut_back U32 v i (U32.ofInt 0 (by intlit))
+ let i1 ← i + (Usize.ofInt 1)
+ let v0 ← Vec.index_mut_back U32 v i (U32.ofInt 0)
clear_loop v0 i1
else Result.ret v
/- [loops::clear]: merged forward/backward function
(there is a single backward function, and the forward function returns ()) -/
def clear (v : Vec U32) : Result (Vec U32) :=
- clear_loop v (Usize.ofInt 0 (by intlit))
+ clear_loop v (Usize.ofInt 0)
/- [loops::list_mem]: loop 0: forward function -/
divergent def list_mem_loop (x : U32) (ls : List U32) : Result Bool :=
@@ -85,12 +82,11 @@ divergent def list_nth_mut_loop_loop
(T : Type) (ls : List T) (i : U32) : Result T :=
match ls with
| List.Cons x tl =>
- if i = (U32.ofInt 0 (by intlit))
+ if i = (U32.ofInt 0)
then Result.ret x
- else
- do
- let i0 ← i - (U32.ofInt 1 (by intlit))
- list_nth_mut_loop_loop T tl i0
+ else do
+ let i0 ← i - (U32.ofInt 1)
+ list_nth_mut_loop_loop T tl i0
| List.Nil => Result.fail Error.panic
/- [loops::list_nth_mut_loop]: forward function -/
@@ -102,11 +98,11 @@ divergent def list_nth_mut_loop_loop_back
(T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) :=
match ls with
| List.Cons x tl =>
- if i = (U32.ofInt 0 (by intlit))
+ if i = (U32.ofInt 0)
then Result.ret (List.Cons ret0 tl)
else
do
- let i0 ← i - (U32.ofInt 1 (by intlit))
+ let i0 ← i - (U32.ofInt 1)
let tl0 ← list_nth_mut_loop_loop_back T tl i0 ret0
Result.ret (List.Cons x tl0)
| List.Nil => Result.fail Error.panic
@@ -121,12 +117,11 @@ 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 = (U32.ofInt 0 (by intlit))
+ if i = (U32.ofInt 0)
then Result.ret x
- else
- do
- let i0 ← i - (U32.ofInt 1 (by intlit))
- list_nth_shared_loop_loop T tl i0
+ else do
+ let i0 ← i - (U32.ofInt 1)
+ list_nth_shared_loop_loop T tl i0
| List.Nil => Result.fail Error.panic
/- [loops::list_nth_shared_loop]: forward function -/
@@ -144,7 +139,7 @@ divergent def get_elem_mut_loop (x : Usize) (ls : List Usize) : Result Usize :=
/- [loops::get_elem_mut]: forward function -/
def get_elem_mut (slots : Vec (List Usize)) (x : Usize) : Result Usize :=
do
- let l ← Vec.index_mut (List Usize) slots (Usize.ofInt 0 (by intlit))
+ let l ← Vec.index_mut (List Usize) slots (Usize.ofInt 0)
get_elem_mut_loop x l
/- [loops::get_elem_mut]: loop 0: backward function 0 -/
@@ -166,9 +161,9 @@ def get_elem_mut_back
Result (Vec (List Usize))
:=
do
- let l ← Vec.index_mut (List Usize) slots (Usize.ofInt 0 (by intlit))
+ let l ← Vec.index_mut (List Usize) slots (Usize.ofInt 0)
let l0 ← get_elem_mut_loop_back x l ret0
- Vec.index_mut_back (List Usize) slots (Usize.ofInt 0 (by intlit)) l0
+ Vec.index_mut_back (List Usize) slots (Usize.ofInt 0) l0
/- [loops::get_elem_shared]: loop 0: forward function -/
divergent def get_elem_shared_loop
@@ -182,7 +177,7 @@ divergent def get_elem_shared_loop
/- [loops::get_elem_shared]: forward function -/
def get_elem_shared (slots : Vec (List Usize)) (x : Usize) : Result Usize :=
do
- let l ← Vec.index (List Usize) slots (Usize.ofInt 0 (by intlit))
+ let l ← Vec.index (List Usize) slots (Usize.ofInt 0)
get_elem_shared_loop x l
/- [loops::id_mut]: forward function -/
@@ -202,12 +197,11 @@ divergent def list_nth_mut_loop_with_id_loop
(T : Type) (i : U32) (ls : List T) : Result T :=
match ls with
| List.Cons x tl =>
- if i = (U32.ofInt 0 (by intlit))
+ if i = (U32.ofInt 0)
then Result.ret x
- else
- do
- let i0 ← i - (U32.ofInt 1 (by intlit))
- list_nth_mut_loop_with_id_loop T i0 tl
+ else do
+ let i0 ← i - (U32.ofInt 1)
+ list_nth_mut_loop_with_id_loop T i0 tl
| List.Nil => Result.fail Error.panic
/- [loops::list_nth_mut_loop_with_id]: forward function -/
@@ -221,11 +215,11 @@ divergent def list_nth_mut_loop_with_id_loop_back
(T : Type) (i : U32) (ls : List T) (ret0 : T) : Result (List T) :=
match ls with
| List.Cons x tl =>
- if i = (U32.ofInt 0 (by intlit))
+ if i = (U32.ofInt 0)
then Result.ret (List.Cons ret0 tl)
else
do
- let i0 ← i - (U32.ofInt 1 (by intlit))
+ let i0 ← i - (U32.ofInt 1)
let tl0 ← list_nth_mut_loop_with_id_loop_back T i0 tl ret0
Result.ret (List.Cons x tl0)
| List.Nil => Result.fail Error.panic
@@ -243,11 +237,11 @@ 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 = (U32.ofInt 0 (by intlit))
+ if i = (U32.ofInt 0)
then Result.ret x
else
do
- let i0 ← i - (U32.ofInt 1 (by intlit))
+ let i0 ← i - (U32.ofInt 1)
list_nth_shared_loop_with_id_loop T i0 tl
| List.Nil => Result.fail Error.panic
@@ -265,11 +259,11 @@ divergent def list_nth_mut_loop_pair_loop
| List.Cons x0 tl0 =>
match ls1 with
| List.Cons x1 tl1 =>
- if i = (U32.ofInt 0 (by intlit))
+ if i = (U32.ofInt 0)
then Result.ret (x0, x1)
else
do
- let i0 ← i - (U32.ofInt 1 (by intlit))
+ let i0 ← i - (U32.ofInt 1)
list_nth_mut_loop_pair_loop T tl0 tl1 i0
| List.Nil => Result.fail Error.panic
| List.Nil => Result.fail Error.panic
@@ -288,11 +282,11 @@ divergent def list_nth_mut_loop_pair_loop_back'a
| List.Cons x0 tl0 =>
match ls1 with
| List.Cons x1 tl1 =>
- if i = (U32.ofInt 0 (by intlit))
+ if i = (U32.ofInt 0)
then Result.ret (List.Cons ret0 tl0)
else
do
- let i0 ← i - (U32.ofInt 1 (by intlit))
+ let i0 ← i - (U32.ofInt 1)
let tl00 ← list_nth_mut_loop_pair_loop_back'a T tl0 tl1 i0 ret0
Result.ret (List.Cons x0 tl00)
| List.Nil => Result.fail Error.panic
@@ -314,11 +308,11 @@ divergent def list_nth_mut_loop_pair_loop_back'b
| List.Cons x0 tl0 =>
match ls1 with
| List.Cons x1 tl1 =>
- if i = (U32.ofInt 0 (by intlit))
+ if i = (U32.ofInt 0)
then Result.ret (List.Cons ret0 tl1)
else
do
- let i0 ← i - (U32.ofInt 1 (by intlit))
+ let i0 ← i - (U32.ofInt 1)
let tl10 ← list_nth_mut_loop_pair_loop_back'b T tl0 tl1 i0 ret0
Result.ret (List.Cons x1 tl10)
| List.Nil => Result.fail Error.panic
@@ -338,11 +332,11 @@ divergent def list_nth_shared_loop_pair_loop
| List.Cons x0 tl0 =>
match ls1 with
| List.Cons x1 tl1 =>
- if i = (U32.ofInt 0 (by intlit))
+ if i = (U32.ofInt 0)
then Result.ret (x0, x1)
else
do
- let i0 ← i - (U32.ofInt 1 (by intlit))
+ let i0 ← i - (U32.ofInt 1)
list_nth_shared_loop_pair_loop T tl0 tl1 i0
| List.Nil => Result.fail Error.panic
| List.Nil => Result.fail Error.panic
@@ -359,11 +353,11 @@ divergent def list_nth_mut_loop_pair_merge_loop
| List.Cons x0 tl0 =>
match ls1 with
| List.Cons x1 tl1 =>
- if i = (U32.ofInt 0 (by intlit))
+ if i = (U32.ofInt 0)
then Result.ret (x0, x1)
else
do
- let i0 ← i - (U32.ofInt 1 (by intlit))
+ let i0 ← i - (U32.ofInt 1)
list_nth_mut_loop_pair_merge_loop T tl0 tl1 i0
| List.Nil => Result.fail Error.panic
| List.Nil => Result.fail Error.panic
@@ -382,12 +376,12 @@ divergent def list_nth_mut_loop_pair_merge_loop_back
| List.Cons x0 tl0 =>
match ls1 with
| List.Cons x1 tl1 =>
- if i = (U32.ofInt 0 (by intlit))
+ if i = (U32.ofInt 0)
then let (t, t0) := ret0
Result.ret (List.Cons t tl0, List.Cons t0 tl1)
else
do
- let i0 ← i - (U32.ofInt 1 (by intlit))
+ let i0 ← i - (U32.ofInt 1)
let (tl00, tl10) ←
list_nth_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
Result.ret (List.Cons x0 tl00, List.Cons x1 tl10)
@@ -408,11 +402,11 @@ divergent def list_nth_shared_loop_pair_merge_loop
| List.Cons x0 tl0 =>
match ls1 with
| List.Cons x1 tl1 =>
- if i = (U32.ofInt 0 (by intlit))
+ if i = (U32.ofInt 0)
then Result.ret (x0, x1)
else
do
- let i0 ← i - (U32.ofInt 1 (by intlit))
+ let i0 ← i - (U32.ofInt 1)
list_nth_shared_loop_pair_merge_loop T tl0 tl1 i0
| List.Nil => Result.fail Error.panic
| List.Nil => Result.fail Error.panic
@@ -429,11 +423,11 @@ divergent def list_nth_mut_shared_loop_pair_loop
| List.Cons x0 tl0 =>
match ls1 with
| List.Cons x1 tl1 =>
- if i = (U32.ofInt 0 (by intlit))
+ if i = (U32.ofInt 0)
then Result.ret (x0, x1)
else
do
- let i0 ← i - (U32.ofInt 1 (by intlit))
+ let i0 ← i - (U32.ofInt 1)
list_nth_mut_shared_loop_pair_loop T tl0 tl1 i0
| List.Nil => Result.fail Error.panic
| List.Nil => Result.fail Error.panic
@@ -452,11 +446,11 @@ divergent def list_nth_mut_shared_loop_pair_loop_back
| List.Cons x0 tl0 =>
match ls1 with
| List.Cons x1 tl1 =>
- if i = (U32.ofInt 0 (by intlit))
+ if i = (U32.ofInt 0)
then Result.ret (List.Cons ret0 tl0)
else
do
- let i0 ← i - (U32.ofInt 1 (by intlit))
+ let i0 ← i - (U32.ofInt 1)
let tl00 ←
list_nth_mut_shared_loop_pair_loop_back T tl0 tl1 i0 ret0
Result.ret (List.Cons x0 tl00)
@@ -477,11 +471,11 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop
| List.Cons x0 tl0 =>
match ls1 with
| List.Cons x1 tl1 =>
- if i = (U32.ofInt 0 (by intlit))
+ if i = (U32.ofInt 0)
then Result.ret (x0, x1)
else
do
- let i0 ← i - (U32.ofInt 1 (by intlit))
+ let i0 ← i - (U32.ofInt 1)
list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i0
| List.Nil => Result.fail Error.panic
| List.Nil => Result.fail Error.panic
@@ -500,11 +494,11 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop_back
| List.Cons x0 tl0 =>
match ls1 with
| List.Cons x1 tl1 =>
- if i = (U32.ofInt 0 (by intlit))
+ if i = (U32.ofInt 0)
then Result.ret (List.Cons ret0 tl0)
else
do
- let i0 ← i - (U32.ofInt 1 (by intlit))
+ let i0 ← i - (U32.ofInt 1)
let tl00 ←
list_nth_mut_shared_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
Result.ret (List.Cons x0 tl00)
@@ -525,11 +519,11 @@ divergent def list_nth_shared_mut_loop_pair_loop
| List.Cons x0 tl0 =>
match ls1 with
| List.Cons x1 tl1 =>
- if i = (U32.ofInt 0 (by intlit))
+ if i = (U32.ofInt 0)
then Result.ret (x0, x1)
else
do
- let i0 ← i - (U32.ofInt 1 (by intlit))
+ let i0 ← i - (U32.ofInt 1)
list_nth_shared_mut_loop_pair_loop T tl0 tl1 i0
| List.Nil => Result.fail Error.panic
| List.Nil => Result.fail Error.panic
@@ -548,11 +542,11 @@ divergent def list_nth_shared_mut_loop_pair_loop_back
| List.Cons x0 tl0 =>
match ls1 with
| List.Cons x1 tl1 =>
- if i = (U32.ofInt 0 (by intlit))
+ if i = (U32.ofInt 0)
then Result.ret (List.Cons ret0 tl1)
else
do
- let i0 ← i - (U32.ofInt 1 (by intlit))
+ let i0 ← i - (U32.ofInt 1)
let tl10 ←
list_nth_shared_mut_loop_pair_loop_back T tl0 tl1 i0 ret0
Result.ret (List.Cons x1 tl10)
@@ -573,11 +567,11 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop
| List.Cons x0 tl0 =>
match ls1 with
| List.Cons x1 tl1 =>
- if i = (U32.ofInt 0 (by intlit))
+ if i = (U32.ofInt 0)
then Result.ret (x0, x1)
else
do
- let i0 ← i - (U32.ofInt 1 (by intlit))
+ let i0 ← i - (U32.ofInt 1)
list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i0
| List.Nil => Result.fail Error.panic
| List.Nil => Result.fail Error.panic
@@ -596,11 +590,11 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop_back
| List.Cons x0 tl0 =>
match ls1 with
| List.Cons x1 tl1 =>
- if i = (U32.ofInt 0 (by intlit))
+ if i = (U32.ofInt 0)
then Result.ret (List.Cons ret0 tl1)
else
do
- let i0 ← i - (U32.ofInt 1 (by intlit))
+ let i0 ← i - (U32.ofInt 1)
let tl10 ←
list_nth_shared_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
Result.ret (List.Cons x1 tl10)
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 1c6421bb..bc707fd9 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -53,7 +53,7 @@ def div_test (x : U32) (y : U32) : Result U32 :=
/- [no_nested_borrows::div_test1]: forward function -/
def div_test1 (x : U32) : Result U32 :=
- x / (U32.ofInt 2 (by intlit))
+ x / (U32.ofInt 2)
/- [no_nested_borrows::rem_test]: forward function -/
def rem_test (x : U32) (y : U32) : Result U32 :=
@@ -66,7 +66,7 @@ def cast_test (x : U32) : Result I32 :=
/- [no_nested_borrows::test2]: forward function -/
def test2 : Result Unit :=
do
- let _ ← (U32.ofInt 23 (by intlit)) + (U32.ofInt 44 (by intlit))
+ let _ ← (U32.ofInt 23) + (U32.ofInt 44)
Result.ret ()
/- Unit test for [no_nested_borrows::test2] -/
@@ -81,10 +81,10 @@ def get_max (x : U32) (y : U32) : Result U32 :=
/- [no_nested_borrows::test3]: forward function -/
def test3 : Result Unit :=
do
- let x ← get_max (U32.ofInt 4 (by intlit)) (U32.ofInt 3 (by intlit))
- let y ← get_max (U32.ofInt 10 (by intlit)) (U32.ofInt 11 (by intlit))
+ let x ← get_max (U32.ofInt 4) (U32.ofInt 3)
+ let y ← get_max (U32.ofInt 10) (U32.ofInt 11)
let z ← x + y
- if not (z = (U32.ofInt 15 (by intlit)))
+ if not (z = (U32.ofInt 15))
then Result.fail Error.panic
else Result.ret ()
@@ -94,8 +94,8 @@ def test3 : Result Unit :=
/- [no_nested_borrows::test_neg1]: forward function -/
def test_neg1 : Result Unit :=
do
- let y ← - (I32.ofInt 3 (by intlit))
- if not (y = (I32.ofInt (-(3:Int)) (by intlit)))
+ let y ← - (I32.ofInt 3)
+ if not (y = (I32.ofInt (-(3:Int))))
then Result.fail Error.panic
else Result.ret ()
@@ -104,7 +104,7 @@ def test_neg1 : Result Unit :=
/- [no_nested_borrows::refs_test1]: forward function -/
def refs_test1 : Result Unit :=
- if not ((I32.ofInt 1 (by intlit)) = (I32.ofInt 1 (by intlit)))
+ if not ((I32.ofInt 1) = (I32.ofInt 1))
then Result.fail Error.panic
else Result.ret ()
@@ -113,16 +113,16 @@ def refs_test1 : Result Unit :=
/- [no_nested_borrows::refs_test2]: forward function -/
def refs_test2 : Result Unit :=
- if not ((I32.ofInt 2 (by intlit)) = (I32.ofInt 2 (by intlit)))
+ if not ((I32.ofInt 2) = (I32.ofInt 2))
then Result.fail Error.panic
else
- if not ((I32.ofInt 0 (by intlit)) = (I32.ofInt 0 (by intlit)))
+ if not ((I32.ofInt 0) = (I32.ofInt 0))
then Result.fail Error.panic
else
- if not ((I32.ofInt 2 (by intlit)) = (I32.ofInt 2 (by intlit)))
+ if not ((I32.ofInt 2) = (I32.ofInt 2))
then Result.fail Error.panic
else
- if not ((I32.ofInt 2 (by intlit)) = (I32.ofInt 2 (by intlit)))
+ if not ((I32.ofInt 2) = (I32.ofInt 2))
then Result.fail Error.panic
else Result.ret ()
@@ -138,9 +138,9 @@ def test_list1 : Result Unit :=
/- [no_nested_borrows::test_box1]: forward function -/
def test_box1 : Result Unit :=
- let b := (I32.ofInt 1 (by intlit))
+ let b := (I32.ofInt 1)
let x := b
- if not (x = (I32.ofInt 1 (by intlit)))
+ if not (x = (I32.ofInt 1))
then Result.fail Error.panic
else Result.ret ()
@@ -166,8 +166,8 @@ def test_panic (b : Bool) : Result Unit :=
/- [no_nested_borrows::test_copy_int]: forward function -/
def test_copy_int : Result Unit :=
do
- let y ← copy_int (I32.ofInt 0 (by intlit))
- if not ((I32.ofInt 0 (by intlit)) = y)
+ let y ← copy_int (I32.ofInt 0)
+ if not ((I32.ofInt 0) = y)
then Result.fail Error.panic
else Result.ret ()
@@ -184,7 +184,7 @@ def is_cons (T : Type) (l : List T) : Result Bool :=
def test_is_cons : Result Unit :=
do
let l := List.Nil
- let b ← is_cons I32 (List.Cons (I32.ofInt 0 (by intlit)) l)
+ let b ← is_cons I32 (List.Cons (I32.ofInt 0) l)
if not b
then Result.fail Error.panic
else Result.ret ()
@@ -202,9 +202,9 @@ def split_list (T : Type) (l : List T) : Result (T × (List T)) :=
def test_split_list : Result Unit :=
do
let l := List.Nil
- let p ← split_list I32 (List.Cons (I32.ofInt 0 (by intlit)) l)
+ let p ← split_list I32 (List.Cons (I32.ofInt 0) l)
let (hd, _) := p
- if not (hd = (I32.ofInt 0 (by intlit)))
+ if not (hd = (I32.ofInt 0))
then Result.fail Error.panic
else Result.ret ()
@@ -227,20 +227,17 @@ def choose_back
/- [no_nested_borrows::choose_test]: forward function -/
def choose_test : Result Unit :=
do
- let z ←
- choose I32 true (I32.ofInt 0 (by intlit)) (I32.ofInt 0 (by intlit))
- let z0 ← z + (I32.ofInt 1 (by intlit))
- if not (z0 = (I32.ofInt 1 (by intlit)))
+ let z ← choose I32 true (I32.ofInt 0) (I32.ofInt 0)
+ let z0 ← z + (I32.ofInt 1)
+ if not (z0 = (I32.ofInt 1))
then Result.fail Error.panic
else
do
- let (x, y) ←
- choose_back I32 true (I32.ofInt 0 (by intlit))
- (I32.ofInt 0 (by intlit)) z0
- if not (x = (I32.ofInt 1 (by intlit)))
+ let (x, y) ← choose_back I32 true (I32.ofInt 0) (I32.ofInt 0) z0
+ if not (x = (I32.ofInt 1))
then Result.fail Error.panic
else
- if not (y = (I32.ofInt 0 (by intlit)))
+ if not (y = (I32.ofInt 0))
then Result.fail Error.panic
else Result.ret ()
@@ -268,20 +265,19 @@ end
/- [no_nested_borrows::list_length]: forward function -/
divergent def list_length (T : Type) (l : List T) : Result U32 :=
match l with
- | List.Cons t l1 =>
- do
- let i ← list_length T l1
- (U32.ofInt 1 (by intlit)) + i
- | List.Nil => Result.ret (U32.ofInt 0 (by intlit))
+ | List.Cons t l1 => do
+ let i ← list_length T l1
+ (U32.ofInt 1) + i
+ | List.Nil => Result.ret (U32.ofInt 0)
/- [no_nested_borrows::list_nth_shared]: forward function -/
divergent def list_nth_shared (T : Type) (l : List T) (i : U32) : Result T :=
match l with
| List.Cons x tl =>
- if i = (U32.ofInt 0 (by intlit))
+ if i = (U32.ofInt 0)
then Result.ret x
else do
- let i0 ← i - (U32.ofInt 1 (by intlit))
+ let i0 ← i - (U32.ofInt 1)
list_nth_shared T tl i0
| List.Nil => Result.fail Error.panic
@@ -289,10 +285,10 @@ divergent def list_nth_shared (T : Type) (l : List T) (i : U32) : Result T :=
divergent def list_nth_mut (T : Type) (l : List T) (i : U32) : Result T :=
match l with
| List.Cons x tl =>
- if i = (U32.ofInt 0 (by intlit))
+ if i = (U32.ofInt 0)
then Result.ret x
else do
- let i0 ← i - (U32.ofInt 1 (by intlit))
+ let i0 ← i - (U32.ofInt 1)
list_nth_mut T tl i0
| List.Nil => Result.fail Error.panic
@@ -301,11 +297,11 @@ divergent def list_nth_mut_back
(T : Type) (l : List T) (i : U32) (ret0 : T) : Result (List T) :=
match l with
| List.Cons x tl =>
- if i = (U32.ofInt 0 (by intlit))
+ if i = (U32.ofInt 0)
then Result.ret (List.Cons ret0 tl)
else
do
- let i0 ← i - (U32.ofInt 1 (by intlit))
+ let i0 ← i - (U32.ofInt 1)
let tl0 ← list_nth_mut_back T tl i0 ret0
Result.ret (List.Cons x tl0)
| List.Nil => Result.fail Error.panic
@@ -327,52 +323,47 @@ def list_rev (T : Type) (l : List T) : Result (List T) :=
def test_list_functions : Result Unit :=
do
let l := List.Nil
- let l0 := List.Cons (I32.ofInt 2 (by intlit)) l
- let l1 := List.Cons (I32.ofInt 1 (by intlit)) l0
- let i ← list_length I32 (List.Cons (I32.ofInt 0 (by intlit)) l1)
- if not (i = (U32.ofInt 3 (by intlit)))
+ let l0 := List.Cons (I32.ofInt 2) l
+ let l1 := List.Cons (I32.ofInt 1) l0
+ let i ← list_length I32 (List.Cons (I32.ofInt 0) l1)
+ if not (i = (U32.ofInt 3))
then Result.fail Error.panic
else
do
let i0 ←
- list_nth_shared I32 (List.Cons (I32.ofInt 0 (by intlit)) l1)
- (U32.ofInt 0 (by intlit))
- if not (i0 = (I32.ofInt 0 (by intlit)))
+ list_nth_shared I32 (List.Cons (I32.ofInt 0) l1) (U32.ofInt 0)
+ if not (i0 = (I32.ofInt 0))
then Result.fail Error.panic
else
do
let i1 ←
- list_nth_shared I32 (List.Cons (I32.ofInt 0 (by intlit)) l1)
- (U32.ofInt 1 (by intlit))
- if not (i1 = (I32.ofInt 1 (by intlit)))
+ list_nth_shared I32 (List.Cons (I32.ofInt 0) l1) (U32.ofInt 1)
+ if not (i1 = (I32.ofInt 1))
then Result.fail Error.panic
else
do
let i2 ←
- list_nth_shared I32 (List.Cons (I32.ofInt 0 (by intlit)) l1)
- (U32.ofInt 2 (by intlit))
- if not (i2 = (I32.ofInt 2 (by intlit)))
+ list_nth_shared I32 (List.Cons (I32.ofInt 0) l1)
+ (U32.ofInt 2)
+ if not (i2 = (I32.ofInt 2))
then Result.fail Error.panic
else
do
let ls ←
- list_nth_mut_back I32 (List.Cons
- (I32.ofInt 0 (by intlit)) l1) (U32.ofInt 1 (by intlit))
- (I32.ofInt 3 (by intlit))
- let i3 ← list_nth_shared I32 ls (U32.ofInt 0 (by intlit))
- if not (i3 = (I32.ofInt 0 (by intlit)))
+ list_nth_mut_back I32 (List.Cons (I32.ofInt 0) l1)
+ (U32.ofInt 1) (I32.ofInt 3)
+ let i3 ← list_nth_shared I32 ls (U32.ofInt 0)
+ if not (i3 = (I32.ofInt 0))
then Result.fail Error.panic
else
do
- let i4 ←
- list_nth_shared I32 ls (U32.ofInt 1 (by intlit))
- if not (i4 = (I32.ofInt 3 (by intlit)))
+ let i4 ← list_nth_shared I32 ls (U32.ofInt 1)
+ if not (i4 = (I32.ofInt 3))
then Result.fail Error.panic
else
do
- let i5 ←
- list_nth_shared I32 ls (U32.ofInt 2 (by intlit))
- if not (i5 = (I32.ofInt 2 (by intlit)))
+ let i5 ← list_nth_shared I32 ls (U32.ofInt 2)
+ if not (i5 = (I32.ofInt 2))
then Result.fail Error.panic
else Result.ret ()
@@ -435,15 +426,15 @@ structure StructWithTuple (T1 T2 : Type) where
/- [no_nested_borrows::new_tuple1]: forward function -/
def new_tuple1 : Result (StructWithTuple U32 U32) :=
- Result.ret { p := ((U32.ofInt 1 (by intlit)), (U32.ofInt 2 (by intlit))) }
+ Result.ret { p := ((U32.ofInt 1), (U32.ofInt 2)) }
/- [no_nested_borrows::new_tuple2]: forward function -/
def new_tuple2 : Result (StructWithTuple I16 I16) :=
- Result.ret { p := ((I16.ofInt 1 (by intlit)), (I16.ofInt 2 (by intlit))) }
+ Result.ret { p := ((I16.ofInt 1), (I16.ofInt 2)) }
/- [no_nested_borrows::new_tuple3]: forward function -/
def new_tuple3 : Result (StructWithTuple U64 I64) :=
- Result.ret { p := ((U64.ofInt 1 (by intlit)), (I64.ofInt 2 (by intlit))) }
+ Result.ret { p := ((U64.ofInt 1), (I64.ofInt 2)) }
/- [no_nested_borrows::StructWithPair] -/
structure StructWithPair (T1 T2 : Type) where
@@ -451,32 +442,31 @@ structure StructWithPair (T1 T2 : Type) where
/- [no_nested_borrows::new_pair1]: forward function -/
def new_pair1 : Result (StructWithPair U32 U32) :=
- Result.ret
- { p := { x := (U32.ofInt 1 (by intlit)), y := (U32.ofInt 2 (by intlit)) } }
+ Result.ret { p := { x := (U32.ofInt 1), y := (U32.ofInt 2) } }
/- [no_nested_borrows::test_constants]: forward function -/
def test_constants : Result Unit :=
do
let swt ← new_tuple1
let (i, _) := swt.p
- if not (i = (U32.ofInt 1 (by intlit)))
+ if not (i = (U32.ofInt 1))
then Result.fail Error.panic
else
do
let swt0 ← new_tuple2
let (i0, _) := swt0.p
- if not (i0 = (I16.ofInt 1 (by intlit)))
+ if not (i0 = (I16.ofInt 1))
then Result.fail Error.panic
else
do
let swt1 ← new_tuple3
let (i1, _) := swt1.p
- if not (i1 = (U64.ofInt 1 (by intlit)))
+ if not (i1 = (U64.ofInt 1))
then Result.fail Error.panic
else
do
let swp ← new_pair1
- if not (swp.p.x = (U32.ofInt 1 (by intlit)))
+ if not (swp.p.x = (U32.ofInt 1))
then Result.fail Error.panic
else Result.ret ()
@@ -493,29 +483,29 @@ def test_weird_borrows1 : Result Unit :=
/- [no_nested_borrows::test_mem_replace]: merged forward/backward function
(there is a single backward function, and the forward function returns ()) -/
def test_mem_replace (px : U32) : Result U32 :=
- let y := mem.replace U32 px (U32.ofInt 1 (by intlit))
- if not (y = (U32.ofInt 0 (by intlit)))
+ let y := mem.replace U32 px (U32.ofInt 1)
+ if not (y = (U32.ofInt 0))
then Result.fail Error.panic
- else Result.ret (U32.ofInt 2 (by intlit))
+ else Result.ret (U32.ofInt 2)
/- [no_nested_borrows::test_shared_borrow_bool1]: forward function -/
def test_shared_borrow_bool1 (b : Bool) : Result U32 :=
if b
- then Result.ret (U32.ofInt 0 (by intlit))
- else Result.ret (U32.ofInt 1 (by intlit))
+ then Result.ret (U32.ofInt 0)
+ else Result.ret (U32.ofInt 1)
/- [no_nested_borrows::test_shared_borrow_bool2]: forward function -/
def test_shared_borrow_bool2 : Result U32 :=
- Result.ret (U32.ofInt 0 (by intlit))
+ Result.ret (U32.ofInt 0)
/- [no_nested_borrows::test_shared_borrow_enum1]: forward function -/
def test_shared_borrow_enum1 (l : List U32) : Result U32 :=
match l with
- | List.Cons i l0 => Result.ret (U32.ofInt 1 (by intlit))
- | List.Nil => Result.ret (U32.ofInt 0 (by intlit))
+ | List.Cons i l0 => Result.ret (U32.ofInt 1)
+ | List.Nil => Result.ret (U32.ofInt 0)
/- [no_nested_borrows::test_shared_borrow_enum2]: forward function -/
def test_shared_borrow_enum2 : Result U32 :=
- Result.ret (U32.ofInt 0 (by intlit))
+ Result.ret (U32.ofInt 0)
end no_nested_borrows
diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
index ade65656..cee7128a 100644
--- a/tests/lean/Paper.lean
+++ b/tests/lean/Paper.lean
@@ -7,13 +7,13 @@ namespace paper
/- [paper::ref_incr]: merged forward/backward function
(there is a single backward function, and the forward function returns ()) -/
def ref_incr (x : I32) : Result I32 :=
- x + (I32.ofInt 1 (by intlit))
+ x + (I32.ofInt 1)
/- [paper::test_incr]: forward function -/
def test_incr : Result Unit :=
do
- let x ← ref_incr (I32.ofInt 0 (by intlit))
- if not (x = (I32.ofInt 1 (by intlit)))
+ let x ← ref_incr (I32.ofInt 0)
+ if not (x = (I32.ofInt 1))
then Result.fail Error.panic
else Result.ret ()
@@ -36,20 +36,17 @@ def choose_back
/- [paper::test_choose]: forward function -/
def test_choose : Result Unit :=
do
- let z ←
- choose I32 true (I32.ofInt 0 (by intlit)) (I32.ofInt 0 (by intlit))
- let z0 ← z + (I32.ofInt 1 (by intlit))
- if not (z0 = (I32.ofInt 1 (by intlit)))
+ let z ← choose I32 true (I32.ofInt 0) (I32.ofInt 0)
+ let z0 ← z + (I32.ofInt 1)
+ if not (z0 = (I32.ofInt 1))
then Result.fail Error.panic
else
do
- let (x, y) ←
- choose_back I32 true (I32.ofInt 0 (by intlit))
- (I32.ofInt 0 (by intlit)) z0
- if not (x = (I32.ofInt 1 (by intlit)))
+ let (x, y) ← choose_back I32 true (I32.ofInt 0) (I32.ofInt 0) z0
+ if not (x = (I32.ofInt 1))
then Result.fail Error.panic
else
- if not (y = (I32.ofInt 0 (by intlit)))
+ if not (y = (I32.ofInt 0))
then Result.fail Error.panic
else Result.ret ()
@@ -65,10 +62,10 @@ inductive List (T : Type) :=
divergent def list_nth_mut (T : Type) (l : List T) (i : U32) : Result T :=
match l with
| List.Cons x tl =>
- if i = (U32.ofInt 0 (by intlit))
+ if i = (U32.ofInt 0)
then Result.ret x
else do
- let i0 ← i - (U32.ofInt 1 (by intlit))
+ let i0 ← i - (U32.ofInt 1)
list_nth_mut T tl i0
| List.Nil => Result.fail Error.panic
@@ -77,11 +74,11 @@ divergent def list_nth_mut_back
(T : Type) (l : List T) (i : U32) (ret0 : T) : Result (List T) :=
match l with
| List.Cons x tl =>
- if i = (U32.ofInt 0 (by intlit))
+ if i = (U32.ofInt 0)
then Result.ret (List.Cons ret0 tl)
else
do
- let i0 ← i - (U32.ofInt 1 (by intlit))
+ let i0 ← i - (U32.ofInt 1)
let tl0 ← list_nth_mut_back T tl i0 ret0
Result.ret (List.Cons x tl0)
| List.Nil => Result.fail Error.panic
@@ -92,23 +89,20 @@ divergent def sum (l : List I32) : Result I32 :=
| List.Cons x tl => do
let i ← sum tl
x + i
- | List.Nil => Result.ret (I32.ofInt 0 (by intlit))
+ | List.Nil => Result.ret (I32.ofInt 0)
/- [paper::test_nth]: forward function -/
def test_nth : Result Unit :=
do
let l := List.Nil
- let l0 := List.Cons (I32.ofInt 3 (by intlit)) l
- let l1 := List.Cons (I32.ofInt 2 (by intlit)) l0
- let x ←
- list_nth_mut I32 (List.Cons (I32.ofInt 1 (by intlit)) l1)
- (U32.ofInt 2 (by intlit))
- let x0 ← x + (I32.ofInt 1 (by intlit))
+ let l0 := List.Cons (I32.ofInt 3) l
+ let l1 := List.Cons (I32.ofInt 2) l0
+ let x ← list_nth_mut I32 (List.Cons (I32.ofInt 1) l1) (U32.ofInt 2)
+ let x0 ← x + (I32.ofInt 1)
let l2 ←
- list_nth_mut_back I32 (List.Cons (I32.ofInt 1 (by intlit)) l1)
- (U32.ofInt 2 (by intlit)) x0
+ list_nth_mut_back I32 (List.Cons (I32.ofInt 1) l1) (U32.ofInt 2) x0
let i ← sum l2
- if not (i = (I32.ofInt 7 (by intlit)))
+ if not (i = (I32.ofInt 7))
then Result.fail Error.panic
else Result.ret ()
@@ -120,7 +114,7 @@ def call_choose (p : (U32 × U32)) : Result U32 :=
do
let (px, py) := p
let pz ← choose U32 true px py
- let pz0 ← pz + (U32.ofInt 1 (by intlit))
+ let pz0 ← pz + (U32.ofInt 1)
let (px0, _) ← choose_back U32 true px py pz0
Result.ret px0
diff --git a/tests/lean/lake-manifest.json b/tests/lean/lake-manifest.json
index 75f7010a..8bbfb7cd 100644
--- a/tests/lean/lake-manifest.json
+++ b/tests/lean/lake-manifest.json
@@ -9,9 +9,15 @@
"inputRev?": "v0.0.11"}},
{"path": {"name": "Base", "dir": "./../../backends/lean"}},
{"git":
+ {"url": "https://github.com/mhuisi/lean4-cli.git",
+ "subDir?": null,
+ "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e",
+ "name": "Cli",
+ "inputRev?": "nightly"}},
+ {"git":
{"url": "https://github.com/leanprover-community/mathlib4.git",
"subDir?": null,
- "rev": "bb4fb766e41dd3a64197263ec132c7f9c4b50065",
+ "rev": "82fe7e902b01fe686b91c19550f1e228ad2dec1c",
"name": "mathlib",
"inputRev?": null}},
{"git":
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 02:25:33 +0000