summaryrefslogtreecommitdiff
path: root/tests/lean/External
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean/External')
-rw-r--r--tests/lean/External/Funs.lean16
1 files changed, 8 insertions, 8 deletions
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index 055d7860..55fb07be 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -30,14 +30,14 @@ def swap_back
def test_new_non_zero_u32
(x : U32) (st : State) : Result (State × core.num.nonzero.NonZeroU32) :=
do
- let (st0, opt) ← core.num.nonzero.NonZeroU32.new x st
- core.option.Option.unwrap core.num.nonzero.NonZeroU32 opt st0
+ let (st0, o) ← core.num.nonzero.NonZeroU32.new x st
+ core.option.Option.unwrap core.num.nonzero.NonZeroU32 o st0
/- [external::test_vec]: forward function -/
def test_vec : Result Unit :=
do
- let v := Vec.new U32
- let _ ← Vec.push U32 v (U32.ofInt 0)
+ let v := alloc.vec.Vec.new U32
+ let _ ← alloc.vec.Vec.push U32 v 0#u32
Result.ret ()
/- Unit test for [external::test_vec] -/
@@ -75,14 +75,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) st0
+ custom_swap_back U32 x y st 1#u32 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) st
- let (st1, (x0, _)) ← swap_back U32 x (U32.ofInt 0) st st0
- if x0 = (U32.ofInt 0)
+ let (st0, _) ← swap U32 x 0#u32 st
+ let (st1, (x0, _)) ← swap_back U32 x 0#u32 st st0
+ if x0 = 0#u32
then Result.fail Error.panic
else Result.ret (st1, x0)