Merge branch 'son/clean' into checked-ops

4 files changed, 15 insertions, 11 deletions

diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index 8b645037..78e0f95c 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -26,10 +26,10 @@ def test_new_non_zero_u32
 def test_vec : Result Unit :=
   do
   let _ ← alloc.vec.Vec.push U32 (alloc.vec.Vec.new U32) 0#u32
-  Result.ret ()
+  Result.ok ()
 
 /- Unit test for [external::test_vec] -/
-#assert (test_vec == Result.ret ())
+#assert (test_vec == Result.ok ())
 
 /- [external::custom_swap]:
    Source: 'src/external.rs', lines 24:0-24:66 -/
@@ -39,8 +39,8 @@ def custom_swap
   :=
   do
   let (st1, (x1, y1)) ← core.mem.swap T x y st
-  let back_'a := fun ret st2 => Result.ret (st2, (ret, y1))
-  Result.ret (st1, (x1, back_'a))
+  let back := fun ret st2 => Result.ok (st2, (ret, y1))
+  Result.ok (st1, (x1, back))
 
 /- [external::test_custom_swap]:
    Source: 'src/external.rs', lines 29:0-29:59 -/
@@ -49,7 +49,7 @@ def test_custom_swap
   do
   let (st1, (_, custom_swap_back)) ← custom_swap U32 x y st
   let (_, (x1, y1)) ← custom_swap_back 1#u32 st1
-  Result.ret (st1, (x1, y1))
+  Result.ok (st1, (x1, y1))
 
 /- [external::test_swap_non_zero]:
    Source: 'src/external.rs', lines 35:0-35:44 -/
@@ -59,6 +59,6 @@ def test_swap_non_zero (x : U32) (st : State) : Result (State × U32) :=
   let (x1, _) := p
   if x1 = 0#u32
   then Result.fail .panic
-  else Result.ret (st1, x1)
+  else Result.ok (st1, x1)
 
 end external
diff --git a/tests/lean/External/FunsExternal.lean b/tests/lean/External/FunsExternal.lean
index 63830abc..b6efc65f 100644
--- a/tests/lean/External/FunsExternal.lean
+++ b/tests/lean/External/FunsExternal.lean
@@ -9,7 +9,7 @@ open external
 /- [core::mem::swap] -/
 def core.mem.swap
   (T : Type) : T → T → State → Result (State × (T × T)) :=
-  fun x y s => .ret (s, (y, x))
+  fun x y s => .ok (s, (y, x))
 
 /- [core::num::nonzero::NonZeroU32::{14}::new] -/
 def core.num.nonzero.NonZeroU32.new :
diff --git a/tests/lean/External/FunsExternal_Template.lean b/tests/lean/External/FunsExternal_Template.lean
index 7e237369..38151dc9 100644
--- a/tests/lean/External/FunsExternal_Template.lean
+++ b/tests/lean/External/FunsExternal_Template.lean
@@ -7,17 +7,20 @@ open Primitives
 open external
 
 /- [core::mem::swap]:
-   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 -/
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42
+   Name pattern: core::mem::swap -/
 axiom core.mem.swap
   (T : Type) : T → T → State → Result (State × (T × T))
 
 /- [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]:
-   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 -/
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57
+   Name pattern: core::num::nonzero::{core::num::nonzero::NonZeroU32}::new -/
 axiom core.num.nonzero.NonZeroU32.new
   : U32 → State → Result (State × (Option core.num.nonzero.NonZeroU32))
 
 /- [core::option::{core::option::Option<T>}::unwrap]:
-   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 -/
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
+   Name pattern: core::option::{core::option::Option<@T>}::unwrap -/
 axiom core.option.Option.unwrap
   (T : Type) : Option T → State → Result (State × T)
 
diff --git a/tests/lean/External/TypesExternal_Template.lean b/tests/lean/External/TypesExternal_Template.lean
index 85fef236..84245531 100644
--- a/tests/lean/External/TypesExternal_Template.lean
+++ b/tests/lean/External/TypesExternal_Template.lean
@@ -5,7 +5,8 @@ import Base
 open Primitives
 
 /- [core::num::nonzero::NonZeroU32]
-   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 -/
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33
+   Name pattern: core::num::nonzero::NonZeroU32 -/
 axiom core.num.nonzero.NonZeroU32 : Type
 
 /- The state type used in the state-error monad -/