Merge branch 'son/clean' into checked-ops

22 files changed, 479 insertions, 467 deletions

diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index 207f31b9..d606640a 100644
--- a/tests/lean/Arrays.lean
+++ b/tests/lean/Arrays.lean
@@ -35,19 +35,19 @@ def array_to_mut_slice_
 def array_len (T : Type) (s : Array T 32#usize) : Result Usize :=
   do
   let s1 ← Array.to_slice T 32#usize s
-  Result.ret (Slice.len T s1)
+  Result.ok (Slice.len T s1)
 
 /- [arrays::shared_array_len]:
    Source: 'src/arrays.rs', lines 29:0-29:48 -/
 def shared_array_len (T : Type) (s : Array T 32#usize) : Result Usize :=
   do
   let s1 ← Array.to_slice T 32#usize s
-  Result.ret (Slice.len T s1)
+  Result.ok (Slice.len T s1)
 
 /- [arrays::shared_slice_len]:
    Source: 'src/arrays.rs', lines 33:0-33:44 -/
 def shared_slice_len (T : Type) (s : Slice T) : Result Usize :=
-  Result.ret (Slice.len T s)
+  Result.ok (Slice.len T s)
 
 /- [arrays::index_array_shared]:
    Source: 'src/arrays.rs', lines 37:0-37:57 -/
@@ -105,7 +105,7 @@ def slice_subslice_mut_
     core.slice.index.Slice.index_mut U32 (core.ops.range.Range Usize)
       (core.slice.index.SliceIndexRangeUsizeSliceTInst U32) x
       { start := y, end_ := z }
-  Result.ret (s, index_mut_back)
+  Result.ok (s, index_mut_back)
 
 /- [arrays::array_to_slice_shared_]:
    Source: 'src/arrays.rs', lines 72:0-72:54 -/
@@ -141,7 +141,7 @@ def array_subslice_mut_
       (core.ops.index.IndexMutSliceTIInst U32 (core.ops.range.Range Usize)
       (core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) x
       { start := y, end_ := z }
-  Result.ret (s, index_mut_back)
+  Result.ok (s, index_mut_back)
 
 /- [arrays::index_slice_0]:
    Source: 'src/arrays.rs', lines 88:0-88:38 -/
@@ -175,37 +175,37 @@ def update_update_array
   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.ret ()
+  Result.ok ()
 
 /- [arrays::array_local_deep_copy]:
    Source: 'src/arrays.rs', lines 118:0-118:43 -/
 def array_local_deep_copy (x : Array U32 32#usize) : Result Unit :=
-  Result.ret ()
+  Result.ok ()
 
 /- [arrays::take_array]:
    Source: 'src/arrays.rs', lines 122:0-122:30 -/
 def take_array (a : Array U32 2#usize) : Result Unit :=
-  Result.ret ()
+  Result.ok ()
 
 /- [arrays::take_array_borrow]:
    Source: 'src/arrays.rs', lines 123:0-123:38 -/
 def take_array_borrow (a : Array U32 2#usize) : Result Unit :=
-  Result.ret ()
+  Result.ok ()
 
 /- [arrays::take_slice]:
    Source: 'src/arrays.rs', lines 124:0-124:28 -/
 def take_slice (s : Slice U32) : Result Unit :=
-  Result.ret ()
+  Result.ok ()
 
 /- [arrays::take_mut_slice]:
    Source: 'src/arrays.rs', lines 125:0-125:36 -/
 def take_mut_slice (s : Slice U32) : Result (Slice U32) :=
-  Result.ret s
+  Result.ok s
 
 /- [arrays::const_array]:
    Source: 'src/arrays.rs', lines 127:0-127:32 -/
 def const_array : Result (Array U32 2#usize) :=
-  Result.ret (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+  Result.ok (Array.make U32 2#usize [ 0#u32, 0#u32 ])
 
 /- [arrays::const_slice]:
    Source: 'src/arrays.rs', lines 131:0-131:20 -/
@@ -213,7 +213,7 @@ def const_slice : Result Unit :=
   do
   let _ ←
     Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
-  Result.ret ()
+  Result.ok ()
 
 /- [arrays::take_all]:
    Source: 'src/arrays.rs', lines 141:0-141:17 -/
@@ -229,7 +229,7 @@ def take_all : Result Unit :=
     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.ret ()
+  Result.ok ()
 
 /- [arrays::index_array]:
    Source: 'src/arrays.rs', lines 155:0-155:38 -/
@@ -251,7 +251,7 @@ def index_slice_u32_0 (x : Slice U32) : Result U32 :=
 def index_mut_slice_u32_0 (x : Slice U32) : Result (U32 × (Slice U32)) :=
   do
   let i ← Slice.index_usize U32 x 0#usize
-  Result.ret (i, x)
+  Result.ok (i, x)
 
 /- [arrays::index_all]:
    Source: 'src/arrays.rs', lines 170:0-170:25 -/
@@ -271,7 +271,7 @@ def index_all : Result U32 :=
   let (i7, s2) ← index_mut_slice_u32_0 s1
   let i8 ← i6 + i7
   let _ ← to_slice_mut_back s2
-  Result.ret i8
+  Result.ok i8
 
 /- [arrays::update_array]:
    Source: 'src/arrays.rs', lines 184:0-184:36 -/
@@ -279,7 +279,7 @@ def update_array (x : Array U32 2#usize) : Result Unit :=
   do
   let (_, index_mut_back) ← Array.index_mut_usize U32 2#usize x 0#usize
   let _ ← index_mut_back 1#u32
-  Result.ret ()
+  Result.ok ()
 
 /- [arrays::update_array_mut_borrow]:
    Source: 'src/arrays.rs', lines 187:0-187:48 -/
@@ -306,7 +306,7 @@ def update_all : Result Unit :=
   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.ret ()
+  Result.ok ()
 
 /- [arrays::range_all]:
    Source: 'src/arrays.rs', lines 205:0-205:18 -/
@@ -320,7 +320,7 @@ def range_all : Result Unit :=
       { start := 1#usize, end_ := 3#usize }
   let s1 ← update_mut_slice s
   let _ ← index_mut_back s1
-  Result.ret ()
+  Result.ok ()
 
 /- [arrays::deref_array_borrow]:
    Source: 'src/arrays.rs', lines 214:0-214:46 -/
@@ -333,12 +333,12 @@ def deref_array_mut_borrow
   (x : Array U32 2#usize) : Result (U32 × (Array U32 2#usize)) :=
   do
   let i ← Array.index_usize U32 2#usize x 0#usize
-  Result.ret (i, x)
+  Result.ok (i, x)
 
 /- [arrays::take_array_t]:
    Source: 'src/arrays.rs', lines 227:0-227:31 -/
 def take_array_t (a : Array AB 2#usize) : Result Unit :=
-  Result.ret ()
+  Result.ok ()
 
 /- [arrays::non_copyable_array]:
    Source: 'src/arrays.rs', lines 229:0-229:27 -/
@@ -356,7 +356,7 @@ divergent def sum_loop (s : Slice U32) (sum1 : U32) (i : Usize) : Result U32 :=
     let sum3 ← sum1 + i2
     let i3 ← i + 1#usize
     sum_loop s sum3 i3
-  else Result.ret sum1
+  else Result.ok sum1
 
 /- [arrays::sum]:
    Source: 'src/arrays.rs', lines 242:0-242:28 -/
@@ -377,7 +377,7 @@ divergent def sum2_loop
     let sum3 ← sum1 + i4
     let i5 ← i + 1#usize
     sum2_loop s s2 sum3 i5
-  else Result.ret sum1
+  else Result.ok sum1
 
 /- [arrays::sum2]:
    Source: 'src/arrays.rs', lines 252:0-252:41 -/
@@ -397,7 +397,7 @@ def f0 : Result Unit :=
   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.ret ()
+  Result.ok ()
 
 /- [arrays::f1]:
    Source: 'src/arrays.rs', lines 268:0-268:11 -/
@@ -407,12 +407,12 @@ def f1 : Result Unit :=
     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.ret ()
+  Result.ok ()
 
 /- [arrays::f2]:
    Source: 'src/arrays.rs', lines 273:0-273:17 -/
 def f2 (i : U32) : Result Unit :=
-  Result.ret ()
+  Result.ok ()
 
 /- [arrays::f4]:
    Source: 'src/arrays.rs', lines 282:0-282:54 -/
@@ -438,7 +438,7 @@ def f3 : Result U32 :=
 
 /- [arrays::SZ]
    Source: 'src/arrays.rs', lines 286:0-286:19 -/
-def SZ_body : Result Usize := Result.ret 32#usize
+def SZ_body : Result Usize := Result.ok 32#usize
 def SZ : Usize := eval_global SZ_body
 
 /- [arrays::f5]:
@@ -458,7 +458,7 @@ def ite : Result Unit :=
   let (_, s3) ← index_mut_slice_u32_0 s2
   let _ ← to_slice_mut_back1 s3
   let _ ← to_slice_mut_back s1
-  Result.ret ()
+  Result.ok ()
 
 /- [arrays::zero_slice]: loop 0:
    Source: 'src/arrays.rs', lines 303:0-310:1 -/
@@ -471,7 +471,7 @@ divergent def zero_slice_loop
     let i1 ← i + 1#usize
     let a1 ← index_mut_back 0#u8
     zero_slice_loop a1 i1 len
-  else Result.ret a
+  else Result.ok a
 
 /- [arrays::zero_slice]:
    Source: 'src/arrays.rs', lines 303:0-303:31 -/
@@ -486,7 +486,7 @@ divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit :=
   then do
        let i1 ← i + 1#usize
        iter_mut_slice_loop len i1
-  else Result.ret ()
+  else Result.ok ()
 
 /- [arrays::iter_mut_slice]:
    Source: 'src/arrays.rs', lines 312:0-312:35 -/
@@ -494,7 +494,7 @@ def iter_mut_slice (a : Slice U8) : Result (Slice U8) :=
   do
   let len := Slice.len U8 a
   let _ ← iter_mut_slice_loop len 0#usize
-  Result.ret a
+  Result.ok a
 
 /- [arrays::sum_mut_slice]: loop 0:
    Source: 'src/arrays.rs', lines 320:0-328:1 -/
@@ -508,13 +508,13 @@ divergent def sum_mut_slice_loop
     let s1 ← s + i2
     let i3 ← i + 1#usize
     sum_mut_slice_loop a i3 s1
-  else Result.ret s
+  else Result.ok s
 
 /- [arrays::sum_mut_slice]:
    Source: 'src/arrays.rs', lines 320:0-320:42 -/
 def sum_mut_slice (a : Slice U32) : Result (U32 × (Slice U32)) :=
   do
   let i ← sum_mut_slice_loop a 0#usize 0#u32
-  Result.ret (i, a)
+  Result.ok (i, a)
 
 end arrays
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index ca9b48da..0c31b9bc 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -42,12 +42,12 @@ def betree.store_leaf_node
 def betree.fresh_node_id (counter : U64) : Result (U64 × U64) :=
   do
   let counter1 ← counter + 1#u64
-  Result.ret (counter, counter1)
+  Result.ok (counter, counter1)
 
 /- [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]:
    Source: 'src/betree.rs', lines 206:4-206:20 -/
 def betree.NodeIdCounter.new : Result betree.NodeIdCounter :=
-  Result.ret { next_node_id := 0#u64 }
+  Result.ok { next_node_id := 0#u64 }
 
 /- [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]:
    Source: 'src/betree.rs', lines 210:4-210:36 -/
@@ -55,7 +55,7 @@ def betree.NodeIdCounter.fresh_id
   (self : betree.NodeIdCounter) : Result (U64 × betree.NodeIdCounter) :=
   do
   let i ← self.next_node_id + 1#u64
-  Result.ret (self.next_node_id, { next_node_id := i })
+  Result.ok (self.next_node_id, { next_node_id := i })
 
 /- [betree_main::betree::upsert_update]:
    Source: 'src/betree.rs', lines 234:0-234:70 -/
@@ -64,8 +64,8 @@ def betree.upsert_update
   match prev with
   | none =>
     match st with
-    | betree.UpsertFunState.Add v => Result.ret v
-    | betree.UpsertFunState.Sub _ => Result.ret 0#u64
+    | betree.UpsertFunState.Add v => Result.ok v
+    | betree.UpsertFunState.Sub _ => Result.ok 0#u64
   | some prev1 =>
     match st with
     | betree.UpsertFunState.Add v =>
@@ -73,11 +73,11 @@ def betree.upsert_update
       let margin ← core_u64_max - prev1
       if margin >= v
       then prev1 + v
-      else Result.ret core_u64_max
+      else Result.ok core_u64_max
     | betree.UpsertFunState.Sub v =>
       if prev1 >= v
       then prev1 - v
-      else Result.ret 0#u64
+      else Result.ok 0#u64
 
 /- [betree_main::betree::{betree_main::betree::List<T>#1}::len]:
    Source: 'src/betree.rs', lines 276:4-276:24 -/
@@ -86,7 +86,7 @@ divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
   | betree.List.Cons _ tl => do
                              let i ← betree.List.len T tl
                              1#u64 + i
-  | betree.List.Nil => Result.ret 0#u64
+  | betree.List.Nil => Result.ok 0#u64
 
 /- [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]:
    Source: 'src/betree.rs', lines 284:4-284:51 -/
@@ -95,7 +95,7 @@ divergent def betree.List.split_at
   Result ((betree.List T) × (betree.List T))
   :=
   if n = 0#u64
-  then Result.ret (betree.List.Nil, self)
+  then Result.ok (betree.List.Nil, self)
   else
     match self with
     | betree.List.Cons hd tl =>
@@ -103,7 +103,7 @@ divergent def betree.List.split_at
       let i ← n - 1#u64
       let p ← betree.List.split_at T tl i
       let (ls0, ls1) := p
-      Result.ret (betree.List.Cons hd ls0, ls1)
+      Result.ok (betree.List.Cons hd ls0, ls1)
     | betree.List.Nil => Result.fail .panic
 
 /- [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]:
@@ -111,7 +111,7 @@ divergent def betree.List.split_at
 def betree.List.push_front
   (T : Type) (self : betree.List T) (x : T) : Result (betree.List T) :=
   let (tl, _) := core.mem.replace (betree.List T) self betree.List.Nil
-  Result.ret (betree.List.Cons x tl)
+  Result.ok (betree.List.Cons x tl)
 
 /- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]:
    Source: 'src/betree.rs', lines 306:4-306:32 -/
@@ -119,14 +119,14 @@ def betree.List.pop_front
   (T : Type) (self : betree.List T) : Result (T × (betree.List T)) :=
   let (ls, _) := core.mem.replace (betree.List T) self betree.List.Nil
   match ls with
-  | betree.List.Cons x tl => Result.ret (x, tl)
+  | betree.List.Cons x tl => Result.ok (x, tl)
   | betree.List.Nil => Result.fail .panic
 
 /- [betree_main::betree::{betree_main::betree::List<T>#1}::hd]:
    Source: 'src/betree.rs', lines 318:4-318:22 -/
 def betree.List.hd (T : Type) (self : betree.List T) : Result T :=
   match self with
-  | betree.List.Cons hd _ => Result.ret hd
+  | betree.List.Cons hd _ => Result.ok hd
   | betree.List.Nil => Result.fail .panic
 
 /- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]:
@@ -135,8 +135,8 @@ def betree.ListPairU64T.head_has_key
   (T : Type) (self : betree.List (U64 × T)) (key : U64) : Result Bool :=
   match self with
   | betree.List.Cons hd _ => let (i, _) := hd
-                             Result.ret (i = key)
-  | betree.List.Nil => Result.ret false
+                             Result.ok (i = key)
+  | betree.List.Nil => Result.ok false
 
 /- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]:
    Source: 'src/betree.rs', lines 339:4-339:73 -/
@@ -148,13 +148,13 @@ divergent def betree.ListPairU64T.partition_at_pivot
   | betree.List.Cons hd tl =>
     let (i, t) := hd
     if i >= pivot
-    then Result.ret (betree.List.Nil, betree.List.Cons (i, t) tl)
+    then Result.ok (betree.List.Nil, betree.List.Cons (i, t) tl)
     else
       do
       let p ← betree.ListPairU64T.partition_at_pivot T tl pivot
       let (ls0, ls1) := p
-      Result.ret (betree.List.Cons (i, t) ls0, ls1)
-  | betree.List.Nil => Result.ret (betree.List.Nil, betree.List.Nil)
+      Result.ok (betree.List.Cons (i, t) ls0, ls1)
+  | betree.List.Nil => Result.ok (betree.List.Nil, betree.List.Nil)
 
 /- [betree_main::betree::{betree_main::betree::Leaf#3}::split]:
    Source: 'src/betree.rs', lines 359:4-364:17 -/
@@ -174,7 +174,7 @@ def betree.Leaf.split
   let (st2, _) ← betree.store_leaf_node id1 content1 st1
   let n := betree.Node.Leaf { id := id0, size := params.split_size }
   let n1 := betree.Node.Leaf { id := id1, size := params.split_size }
-  Result.ret (st2, (betree.Internal.mk self.id pivot n n1, node_id_cnt2))
+  Result.ok (st2, (betree.Internal.mk self.id pivot n n1, node_id_cnt2))
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]:
    Source: 'src/betree.rs', lines 789:4-792:34 -/
@@ -187,18 +187,18 @@ divergent def betree.Node.lookup_first_message_for_key
   | betree.List.Cons x next_msgs =>
     let (i, m) := x
     if i >= key
-    then Result.ret (betree.List.Cons (i, m) next_msgs, Result.ret)
+    then Result.ok (betree.List.Cons (i, m) next_msgs, Result.ok)
     else
       do
       let (l, lookup_first_message_for_key_back) ←
         betree.Node.lookup_first_message_for_key key next_msgs
-      let back_'a :=
+      let back :=
         fun ret =>
           do
           let next_msgs1 ← lookup_first_message_for_key_back ret
-          Result.ret (betree.List.Cons (i, m) next_msgs1)
-      Result.ret (l, back_'a)
-  | betree.List.Nil => Result.ret (betree.List.Nil, Result.ret)
+          Result.ok (betree.List.Cons (i, m) next_msgs1)
+      Result.ok (l, back)
+  | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok)
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]:
    Source: 'src/betree.rs', lines 636:4-636:80 -/
@@ -208,12 +208,12 @@ divergent def betree.Node.lookup_in_bindings
   | betree.List.Cons hd tl =>
     let (i, i1) := hd
     if i = key
-    then Result.ret (some i1)
+    then Result.ok (some i1)
     else
       if i > key
-      then Result.ret none
+      then Result.ok none
       else betree.Node.lookup_in_bindings key tl
-  | betree.List.Nil => Result.ret none
+  | betree.List.Nil => Result.ok none
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]:
    Source: 'src/betree.rs', lines 819:4-819:90 -/
@@ -242,7 +242,7 @@ divergent def betree.Node.apply_upserts
     let msgs1 ←
       betree.List.push_front (U64 × betree.Message) msgs (key,
         betree.Message.Insert v)
-    Result.ret (st1, (v, msgs1))
+    Result.ok (st1, (v, msgs1))
 
 /- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]:
    Source: 'src/betree.rs', lines 395:4-395:63 -/
@@ -255,11 +255,11 @@ mutual divergent def betree.Internal.lookup_in_children
   then
     do
     let (st1, (o, n2)) ← betree.Node.lookup n key st
-    Result.ret (st1, (o, betree.Internal.mk i i1 n2 n1))
+    Result.ok (st1, (o, betree.Internal.mk i i1 n2 n1))
   else
     do
     let (st1, (o, n2)) ← betree.Node.lookup n1 key st
-    Result.ret (st1, (o, betree.Internal.mk i i1 n n2))
+    Result.ok (st1, (o, betree.Internal.mk i i1 n n2))
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::lookup]:
    Source: 'src/betree.rs', lines 709:4-709:58 -/
@@ -285,7 +285,7 @@ divergent def betree.Node.lookup
             st1
         let _ ←
           lookup_first_message_for_key_back (betree.List.Cons (k, msg) l)
-        Result.ret (st2, (o, betree.Node.Internal node1))
+        Result.ok (st2, (o, betree.Node.Internal node1))
       else
         match msg with
         | betree.Message.Insert v =>
@@ -293,14 +293,14 @@ divergent def betree.Node.lookup
           let _ ←
             lookup_first_message_for_key_back (betree.List.Cons (k,
               betree.Message.Insert v) l)
-          Result.ret (st1, (some v, betree.Node.Internal (betree.Internal.mk i
+          Result.ok (st1, (some v, betree.Node.Internal (betree.Internal.mk i
             i1 n n1)))
         | betree.Message.Delete =>
           do
           let _ ←
             lookup_first_message_for_key_back (betree.List.Cons (k,
               betree.Message.Delete) l)
-          Result.ret (st1, (none, betree.Node.Internal (betree.Internal.mk i i1
+          Result.ok (st1, (none, betree.Node.Internal (betree.Internal.mk i i1
             n n1)))
         | betree.Message.Upsert ufs =>
           do
@@ -313,20 +313,20 @@ divergent def betree.Node.lookup
           let ⟨ i2, i3, n2, n3 ⟩ := node1
           let msgs1 ← lookup_first_message_for_key_back pending1
           let (st4, _) ← betree.store_internal_node i2 msgs1 st3
-          Result.ret (st4, (some v1, betree.Node.Internal (betree.Internal.mk
-            i2 i3 n2 n3)))
+          Result.ok (st4, (some v1, betree.Node.Internal (betree.Internal.mk i2
+            i3 n2 n3)))
     | betree.List.Nil =>
       do
       let (st2, (o, node1)) ←
         betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) key
           st1
       let _ ← lookup_first_message_for_key_back betree.List.Nil
-      Result.ret (st2, (o, betree.Node.Internal node1))
+      Result.ok (st2, (o, betree.Node.Internal node1))
   | betree.Node.Leaf node =>
     do
     let (st1, bindings) ← betree.load_leaf_node node.id st
     let o ← betree.Node.lookup_in_bindings key bindings
-    Result.ret (st1, (o, betree.Node.Leaf node))
+    Result.ok (st1, (o, betree.Node.Leaf node))
 
 end
 
@@ -346,8 +346,8 @@ divergent def betree.Node.filter_messages_for_key
         betree.List.pop_front (U64 × betree.Message) (betree.List.Cons (k, m)
           l)
       betree.Node.filter_messages_for_key key msgs1
-    else Result.ret (betree.List.Cons (k, m) l)
-  | betree.List.Nil => Result.ret betree.List.Nil
+    else Result.ok (betree.List.Cons (k, m) l)
+  | betree.List.Nil => Result.ok betree.List.Nil
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]:
    Source: 'src/betree.rs', lines 689:4-692:34 -/
@@ -364,14 +364,14 @@ divergent def betree.Node.lookup_first_message_after_key
       do
       let (l, lookup_first_message_after_key_back) ←
         betree.Node.lookup_first_message_after_key key next_msgs
-      let back_'a :=
+      let back :=
         fun ret =>
           do
           let next_msgs1 ← lookup_first_message_after_key_back ret
-          Result.ret (betree.List.Cons (k, m) next_msgs1)
-      Result.ret (l, back_'a)
-    else Result.ret (betree.List.Cons (k, m) next_msgs, Result.ret)
-  | betree.List.Nil => Result.ret (betree.List.Nil, Result.ret)
+          Result.ok (betree.List.Cons (k, m) next_msgs1)
+      Result.ok (l, back)
+    else Result.ok (betree.List.Cons (k, m) next_msgs, Result.ok)
+  | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok)
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]:
    Source: 'src/betree.rs', lines 521:4-521:89 -/
@@ -450,7 +450,7 @@ divergent def betree.Node.apply_messages_to_internal
     let (i, m) := new_msg
     let msgs1 ← betree.Node.apply_to_internal msgs i m
     betree.Node.apply_messages_to_internal msgs1 new_msgs_tl
-  | betree.List.Nil => Result.ret msgs
+  | betree.List.Nil => Result.ok msgs
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]:
    Source: 'src/betree.rs', lines 653:4-656:32 -/
@@ -463,18 +463,18 @@ divergent def betree.Node.lookup_mut_in_bindings
   | betree.List.Cons hd tl =>
     let (i, i1) := hd
     if i >= key
-    then Result.ret (betree.List.Cons (i, i1) tl, Result.ret)
+    then Result.ok (betree.List.Cons (i, i1) tl, Result.ok)
     else
       do
       let (l, lookup_mut_in_bindings_back) ←
         betree.Node.lookup_mut_in_bindings key tl
-      let back_'a :=
+      let back :=
         fun ret =>
           do
           let tl1 ← lookup_mut_in_bindings_back ret
-          Result.ret (betree.List.Cons (i, i1) tl1)
-      Result.ret (l, back_'a)
-  | betree.List.Nil => Result.ret (betree.List.Nil, Result.ret)
+          Result.ok (betree.List.Cons (i, i1) tl1)
+      Result.ok (l, back)
+  | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok)
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]:
    Source: 'src/betree.rs', lines 460:4-460:87 -/
@@ -529,7 +529,7 @@ divergent def betree.Node.apply_messages_to_leaf
     let (i, m) := new_msg
     let bindings1 ← betree.Node.apply_to_leaf bindings i m
     betree.Node.apply_messages_to_leaf bindings1 new_msgs_tl
-  | betree.List.Nil => Result.ret bindings
+  | betree.List.Nil => Result.ok bindings
 
 /- [betree_main::betree::{betree_main::betree::Internal#4}::flush]:
    Source: 'src/betree.rs', lines 410:4-415:26 -/
@@ -558,17 +558,17 @@ mutual divergent def betree.Internal.flush
       let (st2, p2) ←
         betree.Node.apply_messages n1 params node_id_cnt1 msgs_right st1
       let (n3, node_id_cnt2) := p2
-      Result.ret (st2, (betree.List.Nil, (betree.Internal.mk i i1 n2 n3,
+      Result.ok (st2, (betree.List.Nil, (betree.Internal.mk i i1 n2 n3,
         node_id_cnt2)))
     else
-      Result.ret (st1, (msgs_right, (betree.Internal.mk i i1 n2 n1,
+      Result.ok (st1, (msgs_right, (betree.Internal.mk i i1 n2 n1,
         node_id_cnt1)))
   else
     do
     let (st1, p1) ←
       betree.Node.apply_messages n1 params node_id_cnt msgs_right st
     let (n2, node_id_cnt1) := p1
-    Result.ret (st1, (msgs_left, (betree.Internal.mk i i1 n n2, node_id_cnt1)))
+    Result.ok (st1, (msgs_left, (betree.Internal.mk i i1 n n2, node_id_cnt1)))
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]:
    Source: 'src/betree.rs', lines 588:4-593:5 -/
@@ -594,12 +594,12 @@ divergent def betree.Node.apply_messages
       let (node1, node_id_cnt1) := p
       let ⟨ i2, i3, n2, n3 ⟩ := node1
       let (st3, _) ← betree.store_internal_node i2 content2 st2
-      Result.ret (st3, (betree.Node.Internal (betree.Internal.mk i2 i3 n2 n3),
+      Result.ok (st3, (betree.Node.Internal (betree.Internal.mk i2 i3 n2 n3),
         node_id_cnt1))
     else
       do
       let (st2, _) ← betree.store_internal_node i content1 st1
-      Result.ret (st2, (betree.Node.Internal (betree.Internal.mk i i1 n n1),
+      Result.ok (st2, (betree.Node.Internal (betree.Internal.mk i i1 n n1),
         node_id_cnt))
   | betree.Node.Leaf node =>
     do
@@ -613,11 +613,11 @@ divergent def betree.Node.apply_messages
       let (st2, (new_node, node_id_cnt1)) ←
         betree.Leaf.split node content1 params node_id_cnt st1
       let (st3, _) ← betree.store_leaf_node node.id betree.List.Nil st2
-      Result.ret (st3, (betree.Node.Internal new_node, node_id_cnt1))
+      Result.ok (st3, (betree.Node.Internal new_node, node_id_cnt1))
     else
       do
       let (st2, _) ← betree.store_leaf_node node.id content1 st1
-      Result.ret (st2, (betree.Node.Leaf { node with size := len },
+      Result.ok (st2, (betree.Node.Leaf { node with size := len },
         node_id_cnt))
 
 end
@@ -635,7 +635,7 @@ def betree.Node.apply
     betree.Node.apply_messages self params node_id_cnt (betree.List.Cons (key,
       new_msg) betree.List.Nil) st
   let (self1, node_id_cnt1) := p
-  Result.ret (st1, (self1, node_id_cnt1))
+  Result.ok (st1, (self1, node_id_cnt1))
 
 /- [betree_main::betree::{betree_main::betree::BeTree#6}::new]:
    Source: 'src/betree.rs', lines 849:4-849:60 -/
@@ -647,7 +647,7 @@ def betree.BeTree.new
   let node_id_cnt ← betree.NodeIdCounter.new
   let (id, node_id_cnt1) ← betree.NodeIdCounter.fresh_id node_id_cnt
   let (st1, _) ← betree.store_leaf_node id betree.List.Nil st
-  Result.ret (st1,
+  Result.ok (st1,
     {
       params := { min_flush_size := min_flush_size, split_size := split_size },
       node_id_cnt := node_id_cnt1,
@@ -664,7 +664,7 @@ def betree.BeTree.apply
   let (st1, p) ←
     betree.Node.apply self.root self.params self.node_id_cnt key msg st
   let (n, nic) := p
-  Result.ret (st1, { self with node_id_cnt := nic, root := n })
+  Result.ok (st1, { self with node_id_cnt := nic, root := n })
 
 /- [betree_main::betree::{betree_main::betree::BeTree#6}::insert]:
    Source: 'src/betree.rs', lines 874:4-874:52 -/
@@ -699,14 +699,14 @@ def betree.BeTree.lookup
   :=
   do
   let (st1, (o, n)) ← betree.Node.lookup self.root key st
-  Result.ret (st1, (o, { self with root := n }))
+  Result.ok (st1, (o, { self with root := n }))
 
 /- [betree_main::main]:
    Source: 'src/betree_main.rs', lines 5:0-5:9 -/
 def main : Result Unit :=
-  Result.ret ()
+  Result.ok ()
 
 /- Unit test for [betree_main::main] -/
-#assert (main == Result.ret ())
+#assert (main == Result.ok ())
 
 end betree_main
diff --git a/tests/lean/BetreeMain/FunsExternal_Template.lean b/tests/lean/BetreeMain/FunsExternal_Template.lean
index eaa4b6c2..0b3e4ef4 100644
--- a/tests/lean/BetreeMain/FunsExternal_Template.lean
+++ b/tests/lean/BetreeMain/FunsExternal_Template.lean
@@ -29,7 +29,8 @@ axiom betree_utils.store_leaf_node
   : U64 → betree.List (U64 × U64) → State → Result (State × Unit)
 
 /- [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/Bitwise.lean b/tests/lean/Bitwise.lean
index 7c47e3dd..c13129f1 100644
--- a/tests/lean/Bitwise.lean
+++ b/tests/lean/Bitwise.lean
@@ -22,16 +22,16 @@ def shift_i32 (a : I32) : Result I32 :=
 /- [bitwise::xor_u32]:
    Source: 'src/bitwise.rs', lines 17:0-17:37 -/
 def xor_u32 (a : U32) (b : U32) : Result U32 :=
-  Result.ret (a ^^^ b)
+  Result.ok (a ^^^ b)
 
 /- [bitwise::or_u32]:
    Source: 'src/bitwise.rs', lines 21:0-21:36 -/
 def or_u32 (a : U32) (b : U32) : Result U32 :=
-  Result.ret (a ||| b)
+  Result.ok (a ||| b)
 
 /- [bitwise::and_u32]:
    Source: 'src/bitwise.rs', lines 25:0-25:37 -/
 def and_u32 (a : U32) (b : U32) : Result U32 :=
-  Result.ret (a &&& b)
+  Result.ok (a &&& b)
 
 end bitwise
diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean
index 40f590d4..3cc3ca40 100644
--- a/tests/lean/Constants.lean
+++ b/tests/lean/Constants.lean
@@ -7,17 +7,17 @@ namespace constants
 
 /- [constants::X0]
    Source: 'src/constants.rs', lines 5:0-5:17 -/
-def X0_body : Result U32 := Result.ret 0#u32
+def X0_body : Result U32 := Result.ok 0#u32
 def X0 : U32 := eval_global X0_body
 
 /- [constants::X1]
    Source: 'src/constants.rs', lines 7:0-7:17 -/
-def X1_body : Result U32 := Result.ret core_u32_max
+def X1_body : Result U32 := Result.ok core_u32_max
 def X1 : U32 := eval_global X1_body
 
 /- [constants::X2]
    Source: 'src/constants.rs', lines 10:0-10:17 -/
-def X2_body : Result U32 := Result.ret 3#u32
+def X2_body : Result U32 := Result.ok 3#u32
 def X2 : U32 := eval_global X2_body
 
 /- [constants::incr]:
@@ -33,7 +33,7 @@ def X3 : U32 := eval_global X3_body
 /- [constants::mk_pair0]:
    Source: 'src/constants.rs', lines 23:0-23:51 -/
 def mk_pair0 (x : U32) (y : U32) : Result (U32 × U32) :=
-  Result.ret (x, y)
+  Result.ok (x, y)
 
 /- [constants::Pair]
    Source: 'src/constants.rs', lines 36:0-36:23 -/
@@ -44,7 +44,7 @@ structure Pair (T1 T2 : Type) where
 /- [constants::mk_pair1]:
    Source: 'src/constants.rs', lines 27:0-27:55 -/
 def mk_pair1 (x : U32) (y : U32) : Result (Pair U32 U32) :=
-  Result.ret { x := x, y := y }
+  Result.ok { x := x, y := y }
 
 /- [constants::P0]
    Source: 'src/constants.rs', lines 31:0-31:24 -/
@@ -58,12 +58,12 @@ def P1 : Pair U32 U32 := eval_global P1_body
 
 /- [constants::P2]
    Source: 'src/constants.rs', lines 33:0-33:24 -/
-def P2_body : Result (U32 × U32) := Result.ret (0#u32, 1#u32)
+def P2_body : Result (U32 × U32) := Result.ok (0#u32, 1#u32)
 def P2 : (U32 × U32) := eval_global P2_body
 
 /- [constants::P3]
    Source: 'src/constants.rs', lines 34:0-34:28 -/
-def P3_body : Result (Pair U32 U32) := Result.ret { x := 0#u32, y := 1#u32 }
+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]
@@ -74,7 +74,7 @@ structure Wrap (T : Type) where
 /- [constants::{constants::Wrap<T>}::new]:
    Source: 'src/constants.rs', lines 54:4-54:41 -/
 def Wrap.new (T : Type) (value : T) : Result (Wrap T) :=
-  Result.ret { value := value }
+  Result.ok { value := value }
 
 /- [constants::Y]
    Source: 'src/constants.rs', lines 41:0-41:22 -/
@@ -84,7 +84,7 @@ def Y : Wrap I32 := eval_global Y_body
 /- [constants::unwrap_y]:
    Source: 'src/constants.rs', lines 43:0-43:30 -/
 def unwrap_y : Result I32 :=
-  Result.ret Y.value
+  Result.ok Y.value
 
 /- [constants::YVAL]
    Source: 'src/constants.rs', lines 47:0-47:19 -/
@@ -93,13 +93,13 @@ def YVAL : I32 := eval_global YVAL_body
 
 /- [constants::get_z1::Z1]
    Source: 'src/constants.rs', lines 62:4-62:17 -/
-def get_z1.Z1_body : Result I32 := Result.ret 3#i32
+def get_z1.Z1_body : Result I32 := Result.ok 3#i32
 def get_z1.Z1 : I32 := eval_global get_z1.Z1_body
 
 /- [constants::get_z1]:
    Source: 'src/constants.rs', lines 61:0-61:28 -/
 def get_z1 : Result I32 :=
-  Result.ret get_z1.Z1
+  Result.ok get_z1.Z1
 
 /- [constants::add]:
    Source: 'src/constants.rs', lines 66:0-66:39 -/
@@ -108,12 +108,12 @@ def add (a : I32) (b : I32) : Result I32 :=
 
 /- [constants::Q1]
    Source: 'src/constants.rs', lines 74:0-74:17 -/
-def Q1_body : Result I32 := Result.ret 5#i32
+def Q1_body : Result I32 := Result.ok 5#i32
 def Q1 : I32 := eval_global Q1_body
 
 /- [constants::Q2]
    Source: 'src/constants.rs', lines 75:0-75:17 -/
-def Q2_body : Result I32 := Result.ret Q1
+def Q2_body : Result I32 := Result.ok Q1
 def Q2 : I32 := eval_global Q2_body
 
 /- [constants::Q3]
@@ -131,7 +131,7 @@ def get_z2 : Result I32 :=
 
 /- [constants::S1]
    Source: 'src/constants.rs', lines 80:0-80:18 -/
-def S1_body : Result U32 := Result.ret 6#u32
+def S1_body : Result U32 := Result.ok 6#u32
 def S1 : U32 := eval_global S1_body
 
 /- [constants::S2]
@@ -141,7 +141,7 @@ def S2 : U32 := eval_global S2_body
 
 /- [constants::S3]
    Source: 'src/constants.rs', lines 82:0-82:29 -/
-def S3_body : Result (Pair U32 U32) := Result.ret P3
+def S3_body : Result (Pair U32 U32) := Result.ok P3
 def S3 : Pair U32 U32 := eval_global S3_body
 
 /- [constants::S4]
@@ -156,12 +156,12 @@ structure V (T : Type) (N : Usize) where
 
 /- [constants::{constants::V<T, N>#1}::LEN]
    Source: 'src/constants.rs', lines 91:4-91:24 -/
-def V.LEN_body (T : Type) (N : Usize) : Result Usize := Result.ret N
+def V.LEN_body (T : Type) (N : Usize) : Result Usize := Result.ok N
 def V.LEN (T : Type) (N : Usize) : Usize := eval_global (V.LEN_body T N)
 
 /- [constants::use_v]:
    Source: 'src/constants.rs', lines 94:0-94:42 -/
 def use_v (T : Type) (N : Usize) : Result Usize :=
-  Result.ret (V.LEN T N)
+  Result.ok (V.LEN T N)
 
 end constants
diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
index 4acc69c8..3a3aeb96 100644
--- a/tests/lean/Demo/Demo.lean
+++ b/tests/lean/Demo/Demo.lean
@@ -12,10 +12,10 @@ def choose
   Result (T × (T → Result (T × T)))
   :=
   if b
-  then let back_'a := fun ret => Result.ret (ret, y)
-       Result.ret (x, back_'a)
-  else let back_'a := fun ret => Result.ret (x, ret)
-       Result.ret (y, back_'a)
+  then let back := fun ret => Result.ok (ret, y)
+       Result.ok (x, back)
+  else let back := fun ret => Result.ok (x, ret)
+       Result.ok (y, back)
 
 /- [demo::mul2_add1]:
    Source: 'src/demo.rs', lines 13:0-13:31 -/
@@ -43,7 +43,7 @@ def use_incr : Result Unit :=
   let x ← incr 0#u32
   let x1 ← incr x
   let _ ← incr x1
-  Result.ret ()
+  Result.ok ()
 
 /- [demo::CList]
    Source: 'src/demo.rs', lines 34:0-34:17 -/
@@ -57,7 +57,7 @@ divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T :=
   match l with
   | CList.CCons x tl =>
     if i = 0#u32
-    then Result.ret x
+    then Result.ok x
     else do
          let i1 ← i - 1#u32
          list_nth T tl i1
@@ -73,18 +73,18 @@ divergent def list_nth_mut
   | CList.CCons x tl =>
     if i = 0#u32
     then
-      let back_'a := fun ret => Result.ret (CList.CCons ret tl)
-      Result.ret (x, back_'a)
+      let back := fun ret => Result.ok (CList.CCons ret tl)
+      Result.ok (x, back)
     else
       do
       let i1 ← i - 1#u32
       let (t, list_nth_mut_back) ← list_nth_mut T tl i1
-      let back_'a :=
+      let back :=
         fun ret =>
           do
           let tl1 ← list_nth_mut_back ret
-          Result.ret (CList.CCons x tl1)
-      Result.ret (t, back_'a)
+          Result.ok (CList.CCons x tl1)
+      Result.ok (t, back)
   | CList.CNil => Result.fail .panic
 
 /- [demo::list_nth_mut1]: loop 0:
@@ -97,17 +97,17 @@ divergent def list_nth_mut1_loop
   | CList.CCons x tl =>
     if i = 0#u32
     then
-      let back_'a := fun ret => Result.ret (CList.CCons ret tl)
-      Result.ret (x, back_'a)
+      let back := fun ret => Result.ok (CList.CCons ret tl)
+      Result.ok (x, back)
     else
       do
       let i1 ← i - 1#u32
-      let (t, back_'a) ← list_nth_mut1_loop T tl i1
-      let back_'a1 :=
+      let (t, back) ← list_nth_mut1_loop T tl i1
+      let back1 :=
         fun ret => do
-                   let tl1 ← back_'a ret
-                   Result.ret (CList.CCons x tl1)
-      Result.ret (t, back_'a1)
+                   let tl1 ← back ret
+                   Result.ok (CList.CCons x tl1)
+      Result.ok (t, back1)
   | CList.CNil => Result.fail .panic
 
 /- [demo::list_nth_mut1]:
@@ -122,7 +122,7 @@ def list_nth_mut1
    Source: 'src/demo.rs', lines 80:0-80:28 -/
 divergent def i32_id (i : I32) : Result I32 :=
   if i = 0#i32
-  then Result.ret 0#i32
+  then Result.ok 0#i32
   else do
        let i1 ← i - 1#i32
        let i2 ← i32_id i1
@@ -138,13 +138,13 @@ divergent def list_tail
   | CList.CCons t tl =>
     do
     let (c, list_tail_back) ← list_tail T tl
-    let back_'a :=
+    let back :=
       fun ret =>
         do
         let tl1 ← list_tail_back ret
-        Result.ret (CList.CCons t tl1)
-    Result.ret (c, back_'a)
-  | CList.CNil => Result.ret (CList.CNil, Result.ret)
+        Result.ok (CList.CCons t tl1)
+    Result.ok (c, back)
+  | CList.CNil => Result.ok (CList.CNil, Result.ok)
 
 /- Trait declaration: [demo::Counter]
    Source: 'src/demo.rs', lines 97:0-97:17 -/
@@ -156,7 +156,7 @@ structure Counter (Self : Type) where
 def CounterUsize.incr (self : Usize) : Result (Usize × Usize) :=
   do
   let self1 ← self + 1#usize
-  Result.ret (self, self1)
+  Result.ok (self, self1)
 
 /- Trait implementation: [demo::{(demo::Counter for usize)}]
    Source: 'src/demo.rs', lines 101:0-101:22 -/
diff --git a/tests/lean/Demo/Properties.lean b/tests/lean/Demo/Properties.lean
index e514ac3e..abdc2985 100644
--- a/tests/lean/Demo/Properties.lean
+++ b/tests/lean/Demo/Properties.lean
@@ -9,7 +9,7 @@ namespace demo
 
 -- @[pspec]
 theorem mul2_add1_spec (x : U32) (h : 2 * ↑x + 1 ≤ U32.max)
-  : ∃ y, mul2_add1 x = ret y ∧
+  : ∃ y, mul2_add1 x = ok y ∧
   ↑y = 2 * ↑x + (1 : Int)
   := by
   rw [mul2_add1]
@@ -18,7 +18,7 @@ theorem mul2_add1_spec (x : U32) (h : 2 * ↑x + 1 ≤ U32.max)
   simp; scalar_tac
 
 theorem use_mul2_add1_spec (x : U32) (y : U32) (h : 2 * ↑x + 1 + ↑y ≤ U32.max) :
-  ∃ z, use_mul2_add1 x y = ret z ∧
+  ∃ z, use_mul2_add1 x y = ok z ∧
   ↑z = 2 * ↑x + (1 : Int) + ↑y := by
   rw [use_mul2_add1]
   progress with mul2_add1_spec as ⟨ i ⟩
@@ -34,7 +34,7 @@ open CList
 
 theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
   (h : ↑i < l.to_list.len) :
-  ∃ x, list_nth T l i = ret x ∧
+  ∃ x, list_nth T l i = ok x ∧
   x = l.to_list.index ↑i
   := by
   rw [list_nth]
@@ -52,7 +52,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
       simp_all
 
 theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) :
-  ∃ y, i32_id x = ret y ∧ x.val = y.val := by
+  ∃ y, i32_id x = ok y ∧ x.val = y.val := by
   rw [i32_id]
   if hx : x = 0#i32 then
     simp_all
@@ -66,8 +66,8 @@ termination_by x.val.toNat
 decreasing_by scalar_decr_tac
 
 theorem list_tail_spec {T : Type} [Inhabited T] (l : CList T) :
-  ∃ back, list_tail T l = ret (CList.CNil, back) ∧
-  ∀ tl', ∃ l', back tl' = ret l' ∧ l'.to_list = l.to_list ++ tl'.to_list := by
+  ∃ back, list_tail T l = ok (CList.CNil, back) ∧
+  ∀ tl', ∃ l', back tl' = ok l' ∧ l'.to_list = l.to_list ++ tl'.to_list := by
   rw [list_tail]
   match l with
   | CNil =>
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 -/
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 1c95f7c9..9cbd958c 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -9,7 +9,7 @@ namespace hashmap
 /- [hashmap::hash_key]:
    Source: 'src/hashmap.rs', lines 27:0-27:32 -/
 def hash_key (k : Usize) : Result Usize :=
-  Result.ret k
+  Result.ok k
 
 /- [hashmap::{hashmap::HashMap<T>}::allocate_slots]: loop 0:
    Source: 'src/hashmap.rs', lines 50:4-56:5 -/
@@ -23,7 +23,7 @@ divergent def HashMap.allocate_slots_loop
     let slots1 ← alloc.vec.Vec.push (List T) slots List.Nil
     let n1 ← n - 1#usize
     HashMap.allocate_slots_loop T slots1 n1
-  else Result.ret slots
+  else Result.ok slots
 
 /- [hashmap::{hashmap::HashMap<T>}::allocate_slots]:
    Source: 'src/hashmap.rs', lines 50:4-50:76 -/
@@ -44,7 +44,7 @@ def HashMap.new_with_capacity
   let slots ← HashMap.allocate_slots T (alloc.vec.Vec.new (List T)) capacity
   let i ← capacity * max_load_dividend
   let i1 ← i / max_load_divisor
-  Result.ret
+  Result.ok
     {
       num_entries := 0#usize,
       max_load_factor := (max_load_dividend, max_load_divisor),
@@ -73,19 +73,19 @@ divergent def HashMap.clear_loop
     let i2 ← i + 1#usize
     let slots1 ← index_mut_back List.Nil
     HashMap.clear_loop T slots1 i2
-  else Result.ret slots
+  else Result.ok slots
 
 /- [hashmap::{hashmap::HashMap<T>}::clear]:
    Source: 'src/hashmap.rs', lines 80:4-80:27 -/
 def HashMap.clear (T : Type) (self : HashMap T) : Result (HashMap T) :=
   do
-  let back ← HashMap.clear_loop T self.slots 0#usize
-  Result.ret { self with num_entries := 0#usize, slots := back }
+  let hm ← HashMap.clear_loop T self.slots 0#usize
+  Result.ok { self with num_entries := 0#usize, slots := hm }
 
 /- [hashmap::{hashmap::HashMap<T>}::len]:
    Source: 'src/hashmap.rs', lines 90:4-90:30 -/
 def HashMap.len (T : Type) (self : HashMap T) : Result Usize :=
-  Result.ret self.num_entries
+  Result.ok self.num_entries
 
 /- [hashmap::{hashmap::HashMap<T>}::insert_in_list]: loop 0:
    Source: 'src/hashmap.rs', lines 97:4-114:5 -/
@@ -96,12 +96,12 @@ divergent def HashMap.insert_in_list_loop
   match ls with
   | List.Cons ckey cvalue tl =>
     if ckey = key
-    then Result.ret (false, List.Cons ckey value tl)
+    then Result.ok (false, List.Cons ckey value tl)
     else
       do
-      let (b, back) ← HashMap.insert_in_list_loop T key value tl
-      Result.ret (b, List.Cons ckey cvalue back)
-  | List.Nil => Result.ret (true, List.Cons key value List.Nil)
+      let (b, tl1) ← HashMap.insert_in_list_loop T key value tl
+      Result.ok (b, List.Cons ckey cvalue tl1)
+  | List.Nil => Result.ok (true, List.Cons key value List.Nil)
 
 /- [hashmap::{hashmap::HashMap<T>}::insert_in_list]:
    Source: 'src/hashmap.rs', lines 97:4-97:71 -/
@@ -130,10 +130,10 @@ def HashMap.insert_no_resize
     do
     let i1 ← self.num_entries + 1#usize
     let v ← index_mut_back l1
-    Result.ret { self with num_entries := i1, slots := v }
+    Result.ok { self with num_entries := i1, slots := v }
   else do
        let v ← index_mut_back l1
-       Result.ret { self with slots := v }
+       Result.ok { self with slots := v }
 
 /- [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]: loop 0:
    Source: 'src/hashmap.rs', lines 183:4-196:5 -/
@@ -144,7 +144,7 @@ divergent def HashMap.move_elements_from_list_loop
     do
     let ntable1 ← HashMap.insert_no_resize T ntable k v
     HashMap.move_elements_from_list_loop T ntable1 tl
-  | List.Nil => Result.ret ntable
+  | List.Nil => Result.ok ntable
 
 /- [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]:
    Source: 'src/hashmap.rs', lines 183:4-183:72 -/
@@ -171,7 +171,7 @@ divergent def HashMap.move_elements_loop
     let i2 ← i + 1#usize
     let slots1 ← index_mut_back l1
     HashMap.move_elements_loop T ntable1 slots1 i2
-  else Result.ret (ntable, slots)
+  else Result.ok (ntable, slots)
 
 /- [hashmap::{hashmap::HashMap<T>}::move_elements]:
    Source: 'src/hashmap.rs', lines 171:4-171:95 -/
@@ -198,13 +198,13 @@ def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) :=
     let ntable ← HashMap.new_with_capacity T i3 i i1
     let p ← HashMap.move_elements T ntable self.slots 0#usize
     let (ntable1, _) := p
-    Result.ret
+    Result.ok
       {
         ntable1
           with
           num_entries := self.num_entries, max_load_factor := (i, i1)
       }
-  else Result.ret { self with max_load_factor := (i, i1) }
+  else Result.ok { self with max_load_factor := (i, i1) }
 
 /- [hashmap::{hashmap::HashMap<T>}::insert]:
    Source: 'src/hashmap.rs', lines 129:4-129:48 -/
@@ -217,7 +217,7 @@ def HashMap.insert
   let i ← HashMap.len T self1
   if i > self1.max_load
   then HashMap.try_resize T self1
-  else Result.ret self1
+  else Result.ok self1
 
 /- [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
    Source: 'src/hashmap.rs', lines 206:4-219:5 -/
@@ -226,9 +226,9 @@ divergent def HashMap.contains_key_in_list_loop
   match ls with
   | List.Cons ckey _ tl =>
     if ckey = key
-    then Result.ret true
+    then Result.ok true
     else HashMap.contains_key_in_list_loop T key tl
-  | List.Nil => Result.ret false
+  | List.Nil => Result.ok false
 
 /- [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]:
    Source: 'src/hashmap.rs', lines 206:4-206:68 -/
@@ -256,7 +256,7 @@ divergent def HashMap.get_in_list_loop
   match ls with
   | List.Cons ckey cvalue tl =>
     if ckey = key
-    then Result.ret cvalue
+    then Result.ok cvalue
     else HashMap.get_in_list_loop T key tl
   | List.Nil => Result.fail .panic
 
@@ -287,17 +287,17 @@ divergent def HashMap.get_mut_in_list_loop
   | List.Cons ckey cvalue tl =>
     if ckey = key
     then
-      let back_'a := fun ret => Result.ret (List.Cons ckey ret tl)
-      Result.ret (cvalue, back_'a)
+      let back := fun ret => Result.ok (List.Cons ckey ret tl)
+      Result.ok (cvalue, back)
     else
       do
-      let (t, back_'a) ← HashMap.get_mut_in_list_loop T tl key
-      let back_'a1 :=
+      let (t, back) ← HashMap.get_mut_in_list_loop T tl key
+      let back1 :=
         fun ret =>
           do
-          let tl1 ← back_'a ret
-          Result.ret (List.Cons ckey cvalue tl1)
-      Result.ret (t, back_'a1)
+          let tl1 ← back ret
+          Result.ok (List.Cons ckey cvalue tl1)
+      Result.ok (t, back1)
   | List.Nil => Result.fail .panic
 
 /- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]:
@@ -322,13 +322,13 @@ def HashMap.get_mut
     alloc.vec.Vec.index_mut (List T) Usize
       (core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots hash_mod
   let (t, get_mut_in_list_back) ← HashMap.get_mut_in_list T l key
-  let back_'a :=
+  let back :=
     fun ret =>
       do
       let l1 ← get_mut_in_list_back ret
       let v ← index_mut_back l1
-      Result.ret { self with slots := v }
-  Result.ret (t, back_'a)
+      Result.ok { self with slots := v }
+  Result.ok (t, back)
 
 /- [hashmap::{hashmap::HashMap<T>}::remove_from_list]: loop 0:
    Source: 'src/hashmap.rs', lines 265:4-291:5 -/
@@ -341,13 +341,13 @@ divergent def HashMap.remove_from_list_loop
       let (mv_ls, _) :=
         core.mem.replace (List T) (List.Cons ckey t tl) List.Nil
       match mv_ls with
-      | List.Cons _ cvalue tl1 => Result.ret (some cvalue, tl1)
+      | List.Cons _ cvalue tl1 => Result.ok (some cvalue, tl1)
       | List.Nil => Result.fail .panic
     else
       do
-      let (o, back) ← HashMap.remove_from_list_loop T key tl
-      Result.ret (o, List.Cons ckey t back)
-  | List.Nil => Result.ret (none, List.Nil)
+      let (o, tl1) ← HashMap.remove_from_list_loop T key tl
+      Result.ok (o, List.Cons ckey t tl1)
+  | List.Nil => Result.ok (none, List.Nil)
 
 /- [hashmap::{hashmap::HashMap<T>}::remove_from_list]:
    Source: 'src/hashmap.rs', lines 265:4-265:69 -/
@@ -373,12 +373,12 @@ def HashMap.remove
   | none =>
     do
     let v ← index_mut_back l1
-    Result.ret (none, { self with slots := v })
+    Result.ok (none, { self with slots := v })
   | some x1 =>
     do
     let i1 ← self.num_entries - 1#usize
     let v ← index_mut_back l1
-    Result.ret (some x1, { self with num_entries := i1, slots := v })
+    Result.ok (some x1, { self with num_entries := i1, slots := v })
 
 /- [hashmap::test1]:
    Source: 'src/hashmap.rs', lines 315:0-315:10 -/
@@ -422,6 +422,6 @@ def test1 : Result Unit :=
               let i4 ← HashMap.get U64 hm6 1056#usize
               if ¬ (i4 = 256#u64)
               then Result.fail .panic
-              else Result.ret ()
+              else Result.ok ()
 
 end hashmap
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index 7215e286..fcaf5806 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -59,7 +59,7 @@ def distinct_keys (ls : Core.List (Usize × α)) := ls.pairwise_rel (λ x y => x
 
 def hash_mod_key (k : Usize) (l : Int) : Int :=
   match hash_key k with
-  | .ret k => k.val % l
+  | .ok k => k.val % l
   | _ => 0
 
 @[simp]
@@ -113,11 +113,15 @@ def inv (hm : HashMap α) : Prop :=
 -- This rewriting lemma is problematic below
 attribute [-simp] Bool.exists_bool
 
+-- The proof below is a bit expensive, so we need to increase the maximum number
+-- of heart beats
+set_option maxHeartbeats 1000000
+
 theorem insert_in_list_spec_aux {α : Type} (l : Int) (key: Usize) (value: α) (l0: List α)
   (hinv : slot_s_inv_hash l (hash_mod_key key l) l0.v)
   (hdk : distinct_keys l0.v) :
   ∃ b l1,
-    insert_in_list α key value l0 = ret (b, l1) ∧
+    insert_in_list α key value l0 = ok (b, l1) ∧
     -- The boolean is true ↔ we inserted a new binding
     (b ↔ (l0.lookup key = none)) ∧
     -- We update the binding
@@ -179,7 +183,7 @@ theorem insert_in_list_spec {α : Type} (l : Int) (key: Usize) (value: α) (l0:
   (hinv : slot_s_inv_hash l (hash_mod_key key l) l0.v)
   (hdk : distinct_keys l0.v) :
   ∃ b l1,
-    insert_in_list α key value l0 = ret (b, l1) ∧
+    insert_in_list α key value l0 = ok (b, l1) ∧
     (b ↔ (l0.lookup key = none)) ∧
     -- We update the binding
     l1.lookup key = value ∧
@@ -232,11 +236,11 @@ set_option pp.coercions false -- do not print coercions with ↑ (this doesn't p
 
 -- The proof below is a bit expensive, so we need to increase the maximum number
 -- of heart beats
-set_option maxHeartbeats 1000000
+set_option maxHeartbeats 2000000
 
 theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value : α)
   (hinv : hm.inv) (hnsat : hm.lookup key = none → hm.len_s < Usize.max) :
-  ∃ nhm, hm.insert_no_resize α key value = ret nhm  ∧
+  ∃ nhm, hm.insert_no_resize α key value = ok nhm  ∧
   -- We preserve the invariant
   nhm.inv ∧
   -- We updated the binding for key
@@ -249,7 +253,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
    | some _ => nhm.len_s = hm.len_s) := by
   rw [insert_no_resize]
   -- Simplify. Note that this also simplifies some function calls, like array index
-  simp [hash_key, bind_tc_ret]
+  simp [hash_key, bind_tc_ok]
   have _ : (alloc.vec.Vec.len (List α) hm.slots).val ≠ 0 := by
    intro
    simp_all [inv]
@@ -277,7 +281,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
   rw [if_update_eq] -- TODO: necessary because we don't have a join
   -- TODO: progress to ...
   have hipost :
-    ∃ i0, (if inserted = true then hm.num_entries + Usize.ofInt 1 else pure hm.num_entries) = ret i0 ∧
+    ∃ i0, (if inserted = true then hm.num_entries + Usize.ofInt 1 else pure hm.num_entries) = ok i0 ∧
     i0.val = if inserted then hm.num_entries.val + 1 else hm.num_entries.val
     := by
     if inserted then
@@ -318,17 +322,21 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value
       simp_all
     have _ : 0 ≤ k_hash_mod := by
       -- TODO: we want to automate this
-      simp
+      simp only [k_hash_mod]
       apply Int.emod_nonneg k.val hvnz
     have _ : k_hash_mod < alloc.vec.Vec.length hm.slots := by
       -- TODO: we want to automate this
-      simp
+      simp only [k_hash_mod]
       have h := Int.emod_lt_of_pos k.val hvpos
-      simp_all
+      simp_all only [ok.injEq, exists_eq_left', List.len_update, gt_iff_lt,
+                     List.index_update_eq, ne_eq, not_false_eq_true, neq_imp]
     if h_hm : k_hash_mod = hash_mod.val then
-      simp_all
+      simp_all only [k_hash_mod, List.len_update, gt_iff_lt, List.index_update_eq,
+                     ne_eq, not_false_eq_true, neq_imp, alloc.vec.Vec.length]
     else
-      simp_all
+      simp_all only [k_hash_mod, List.len_update, gt_iff_lt, List.index_update_eq,
+                     ne_eq, not_false_eq_true, neq_imp, ge_iff_le,
+                     alloc.vec.Vec.length, List.index_update_ne]
   have _ :
     match hm.lookup key with
     | none => nhm.len_s = hm.len_s + 1
diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean
index 6a6934b8..e985ec6a 100644
--- a/tests/lean/HashmapMain/Funs.lean
+++ b/tests/lean/HashmapMain/Funs.lean
@@ -10,7 +10,7 @@ namespace hashmap_main
 /- [hashmap_main::hashmap::hash_key]:
    Source: 'src/hashmap.rs', lines 27:0-27:32 -/
 def hashmap.hash_key (k : Usize) : Result Usize :=
-  Result.ret k
+  Result.ok k
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::allocate_slots]: loop 0:
    Source: 'src/hashmap.rs', lines 50:4-56:5 -/
@@ -24,7 +24,7 @@ divergent def hashmap.HashMap.allocate_slots_loop
     let slots1 ← alloc.vec.Vec.push (hashmap.List T) slots hashmap.List.Nil
     let n1 ← n - 1#usize
     hashmap.HashMap.allocate_slots_loop T slots1 n1
-  else Result.ret slots
+  else Result.ok slots
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::allocate_slots]:
    Source: 'src/hashmap.rs', lines 50:4-50:76 -/
@@ -47,7 +47,7 @@ def hashmap.HashMap.new_with_capacity
       capacity
   let i ← capacity * max_load_dividend
   let i1 ← i / max_load_divisor
-  Result.ret
+  Result.ok
     {
       num_entries := 0#usize,
       max_load_factor := (max_load_dividend, max_load_divisor),
@@ -76,20 +76,20 @@ divergent def hashmap.HashMap.clear_loop
     let i2 ← i + 1#usize
     let slots1 ← index_mut_back hashmap.List.Nil
     hashmap.HashMap.clear_loop T slots1 i2
-  else Result.ret slots
+  else Result.ok slots
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::clear]:
    Source: 'src/hashmap.rs', lines 80:4-80:27 -/
 def hashmap.HashMap.clear
   (T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) :=
   do
-  let back ← hashmap.HashMap.clear_loop T self.slots 0#usize
-  Result.ret { self with num_entries := 0#usize, slots := back }
+  let hm ← hashmap.HashMap.clear_loop T self.slots 0#usize
+  Result.ok { self with num_entries := 0#usize, slots := hm }
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::len]:
    Source: 'src/hashmap.rs', lines 90:4-90:30 -/
 def hashmap.HashMap.len (T : Type) (self : hashmap.HashMap T) : Result Usize :=
-  Result.ret self.num_entries
+  Result.ok self.num_entries
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_in_list]: loop 0:
    Source: 'src/hashmap.rs', lines 97:4-114:5 -/
@@ -100,13 +100,13 @@ divergent def hashmap.HashMap.insert_in_list_loop
   match ls with
   | hashmap.List.Cons ckey cvalue tl =>
     if ckey = key
-    then Result.ret (false, hashmap.List.Cons ckey value tl)
+    then Result.ok (false, hashmap.List.Cons ckey value tl)
     else
       do
-      let (b, back) ← hashmap.HashMap.insert_in_list_loop T key value tl
-      Result.ret (b, hashmap.List.Cons ckey cvalue back)
+      let (b, tl1) ← hashmap.HashMap.insert_in_list_loop T key value tl
+      Result.ok (b, hashmap.List.Cons ckey cvalue tl1)
   | hashmap.List.Nil =>
-    Result.ret (true, hashmap.List.Cons key value hashmap.List.Nil)
+    Result.ok (true, hashmap.List.Cons key value hashmap.List.Nil)
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_in_list]:
    Source: 'src/hashmap.rs', lines 97:4-97:71 -/
@@ -136,10 +136,10 @@ def hashmap.HashMap.insert_no_resize
     do
     let i1 ← self.num_entries + 1#usize
     let v ← index_mut_back l1
-    Result.ret { self with num_entries := i1, slots := v }
+    Result.ok { self with num_entries := i1, slots := v }
   else do
        let v ← index_mut_back l1
-       Result.ret { self with slots := v }
+       Result.ok { self with slots := v }
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements_from_list]: loop 0:
    Source: 'src/hashmap.rs', lines 183:4-196:5 -/
@@ -152,7 +152,7 @@ divergent def hashmap.HashMap.move_elements_from_list_loop
     do
     let ntable1 ← hashmap.HashMap.insert_no_resize T ntable k v
     hashmap.HashMap.move_elements_from_list_loop T ntable1 tl
-  | hashmap.List.Nil => Result.ret ntable
+  | hashmap.List.Nil => Result.ok ntable
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements_from_list]:
    Source: 'src/hashmap.rs', lines 183:4-183:72 -/
@@ -181,7 +181,7 @@ divergent def hashmap.HashMap.move_elements_loop
     let i2 ← i + 1#usize
     let slots1 ← index_mut_back l1
     hashmap.HashMap.move_elements_loop T ntable1 slots1 i2
-  else Result.ret (ntable, slots)
+  else Result.ok (ntable, slots)
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements]:
    Source: 'src/hashmap.rs', lines 171:4-171:95 -/
@@ -209,13 +209,13 @@ def hashmap.HashMap.try_resize
     let ntable ← hashmap.HashMap.new_with_capacity T i3 i i1
     let p ← hashmap.HashMap.move_elements T ntable self.slots 0#usize
     let (ntable1, _) := p
-    Result.ret
+    Result.ok
       {
         ntable1
           with
           num_entries := self.num_entries, max_load_factor := (i, i1)
       }
-  else Result.ret { self with max_load_factor := (i, i1) }
+  else Result.ok { self with max_load_factor := (i, i1) }
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert]:
    Source: 'src/hashmap.rs', lines 129:4-129:48 -/
@@ -228,7 +228,7 @@ def hashmap.HashMap.insert
   let i ← hashmap.HashMap.len T self1
   if i > self1.max_load
   then hashmap.HashMap.try_resize T self1
-  else Result.ret self1
+  else Result.ok self1
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
    Source: 'src/hashmap.rs', lines 206:4-219:5 -/
@@ -237,9 +237,9 @@ divergent def hashmap.HashMap.contains_key_in_list_loop
   match ls with
   | hashmap.List.Cons ckey _ tl =>
     if ckey = key
-    then Result.ret true
+    then Result.ok true
     else hashmap.HashMap.contains_key_in_list_loop T key tl
-  | hashmap.List.Nil => Result.ret false
+  | hashmap.List.Nil => Result.ok false
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]:
    Source: 'src/hashmap.rs', lines 206:4-206:68 -/
@@ -268,7 +268,7 @@ divergent def hashmap.HashMap.get_in_list_loop
   match ls with
   | hashmap.List.Cons ckey cvalue tl =>
     if ckey = key
-    then Result.ret cvalue
+    then Result.ok cvalue
     else hashmap.HashMap.get_in_list_loop T key tl
   | hashmap.List.Nil => Result.fail .panic
 
@@ -302,17 +302,17 @@ divergent def hashmap.HashMap.get_mut_in_list_loop
   | hashmap.List.Cons ckey cvalue tl =>
     if ckey = key
     then
-      let back_'a := fun ret => Result.ret (hashmap.List.Cons ckey ret tl)
-      Result.ret (cvalue, back_'a)
+      let back := fun ret => Result.ok (hashmap.List.Cons ckey ret tl)
+      Result.ok (cvalue, back)
     else
       do
-      let (t, back_'a) ← hashmap.HashMap.get_mut_in_list_loop T tl key
-      let back_'a1 :=
+      let (t, back) ← hashmap.HashMap.get_mut_in_list_loop T tl key
+      let back1 :=
         fun ret =>
           do
-          let tl1 ← back_'a ret
-          Result.ret (hashmap.List.Cons ckey cvalue tl1)
-      Result.ret (t, back_'a1)
+          let tl1 ← back ret
+          Result.ok (hashmap.List.Cons ckey cvalue tl1)
+      Result.ok (t, back1)
   | hashmap.List.Nil => Result.fail .panic
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]:
@@ -338,13 +338,13 @@ def hashmap.HashMap.get_mut
       (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) self.slots
       hash_mod
   let (t, get_mut_in_list_back) ← hashmap.HashMap.get_mut_in_list T l key
-  let back_'a :=
+  let back :=
     fun ret =>
       do
       let l1 ← get_mut_in_list_back ret
       let v ← index_mut_back l1
-      Result.ret { self with slots := v }
-  Result.ret (t, back_'a)
+      Result.ok { self with slots := v }
+  Result.ok (t, back)
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: loop 0:
    Source: 'src/hashmap.rs', lines 265:4-291:5 -/
@@ -360,13 +360,13 @@ divergent def hashmap.HashMap.remove_from_list_loop
         core.mem.replace (hashmap.List T) (hashmap.List.Cons ckey t tl)
           hashmap.List.Nil
       match mv_ls with
-      | hashmap.List.Cons _ cvalue tl1 => Result.ret (some cvalue, tl1)
+      | hashmap.List.Cons _ cvalue tl1 => Result.ok (some cvalue, tl1)
       | hashmap.List.Nil => Result.fail .panic
     else
       do
-      let (o, back) ← hashmap.HashMap.remove_from_list_loop T key tl
-      Result.ret (o, hashmap.List.Cons ckey t back)
-  | hashmap.List.Nil => Result.ret (none, hashmap.List.Nil)
+      let (o, tl1) ← hashmap.HashMap.remove_from_list_loop T key tl
+      Result.ok (o, hashmap.List.Cons ckey t tl1)
+  | hashmap.List.Nil => Result.ok (none, hashmap.List.Nil)
 
 /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]:
    Source: 'src/hashmap.rs', lines 265:4-265:69 -/
@@ -395,12 +395,12 @@ def hashmap.HashMap.remove
   | none =>
     do
     let v ← index_mut_back l1
-    Result.ret (none, { self with slots := v })
+    Result.ok (none, { self with slots := v })
   | some x1 =>
     do
     let i1 ← self.num_entries - 1#usize
     let v ← index_mut_back l1
-    Result.ret (some x1, { self with num_entries := i1, slots := v })
+    Result.ok (some x1, { self with num_entries := i1, slots := v })
 
 /- [hashmap_main::hashmap::test1]:
    Source: 'src/hashmap.rs', lines 315:0-315:10 -/
@@ -444,7 +444,7 @@ def hashmap.test1 : Result Unit :=
               let i4 ← hashmap.HashMap.get U64 hm6 1056#usize
               if ¬ (i4 = 256#u64)
               then Result.fail .panic
-              else Result.ret ()
+              else Result.ok ()
 
 /- [hashmap_main::insert_on_disk]:
    Source: 'src/hashmap_main.rs', lines 7:0-7:43 -/
@@ -458,6 +458,6 @@ def insert_on_disk
 /- [hashmap_main::main]:
    Source: 'src/hashmap_main.rs', lines 16:0-16:13 -/
 def main : Result Unit :=
-  Result.ret ()
+  Result.ok ()
 
 end hashmap_main
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index 0f3d77c2..eeba1add 100644
--- a/tests/lean/Loops.lean
+++ b/tests/lean/Loops.lean
@@ -65,7 +65,7 @@ divergent def sum_array_loop
     let s1 ← s + i1
     let i2 ← i + 1#usize
     sum_array_loop N a i2 s1
-  else Result.ret s
+  else Result.ok s
 
 /- [loops::sum_array]:
    Source: 'src/loops.rs', lines 50:0-50:52 -/
@@ -86,7 +86,7 @@ divergent def clear_loop
     let i2 ← i + 1#usize
     let v1 ← index_mut_back 0#u32
     clear_loop v1 i2
-  else Result.ret v
+  else Result.ok v
 
 /- [loops::clear]:
    Source: 'src/loops.rs', lines 62:0-62:30 -/
@@ -104,9 +104,9 @@ inductive List (T : Type) :=
 divergent def list_mem_loop (x : U32) (ls : List U32) : Result Bool :=
   match ls with
   | List.Cons y tl => if y = x
-                      then Result.ret true
+                      then Result.ok true
                       else list_mem_loop x tl
-  | List.Nil => Result.ret false
+  | List.Nil => Result.ok false
 
 /- [loops::list_mem]:
    Source: 'src/loops.rs', lines 76:0-76:52 -/
@@ -121,8 +121,8 @@ divergent def list_nth_mut_loop_loop
   | List.Cons x tl =>
     if i = 0#u32
     then
-      let back := fun ret => Result.ret (List.Cons ret tl)
-      Result.ret (x, back)
+      let back := fun ret => Result.ok (List.Cons ret tl)
+      Result.ok (x, back)
     else
       do
       let i1 ← i - 1#u32
@@ -130,8 +130,8 @@ divergent def list_nth_mut_loop_loop
       let back1 :=
         fun ret => do
                    let tl1 ← back ret
-                   Result.ret (List.Cons x tl1)
-      Result.ret (t, back1)
+                   Result.ok (List.Cons x tl1)
+      Result.ok (t, back1)
   | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_mut_loop]:
@@ -147,7 +147,7 @@ divergent def list_nth_shared_loop_loop
   match ls with
   | List.Cons x tl =>
     if i = 0#u32
-    then Result.ret x
+    then Result.ok x
     else do
          let i1 ← i - 1#u32
          list_nth_shared_loop_loop T tl i1
@@ -168,16 +168,16 @@ divergent def get_elem_mut_loop
   | List.Cons y tl =>
     if y = x
     then
-      let back := fun ret => Result.ret (List.Cons ret tl)
-      Result.ret (y, back)
+      let back := fun ret => Result.ok (List.Cons ret tl)
+      Result.ok (y, back)
     else
       do
       let (i, back) ← get_elem_mut_loop x tl
       let back1 :=
         fun ret => do
                    let tl1 ← back ret
-                   Result.ret (List.Cons y tl1)
-      Result.ret (i, back1)
+                   Result.ok (List.Cons y tl1)
+      Result.ok (i, back1)
   | List.Nil => Result.fail .panic
 
 /- [loops::get_elem_mut]:
@@ -194,7 +194,7 @@ def get_elem_mut
   let back1 := fun ret => do
                           let l ← back ret
                           index_mut_back l
-  Result.ret (i, back1)
+  Result.ok (i, back1)
 
 /- [loops::get_elem_shared]: loop 0:
    Source: 'src/loops.rs', lines 129:0-143:1 -/
@@ -202,7 +202,7 @@ divergent def get_elem_shared_loop
   (x : Usize) (ls : List Usize) : Result Usize :=
   match ls with
   | List.Cons y tl => if y = x
-                      then Result.ret y
+                      then Result.ok y
                       else get_elem_shared_loop x tl
   | List.Nil => Result.fail .panic
 
@@ -222,12 +222,12 @@ def id_mut
   (T : Type) (ls : List T) :
   Result ((List T) × (List T → Result (List T)))
   :=
-  Result.ret (ls, Result.ret)
+  Result.ok (ls, Result.ok)
 
 /- [loops::id_shared]:
    Source: 'src/loops.rs', lines 149:0-149:45 -/
 def id_shared (T : Type) (ls : List T) : Result (List T) :=
-  Result.ret ls
+  Result.ok ls
 
 /- [loops::list_nth_mut_loop_with_id]: loop 0:
    Source: 'src/loops.rs', lines 154:0-165:1 -/
@@ -237,8 +237,8 @@ divergent def list_nth_mut_loop_with_id_loop
   | List.Cons x tl =>
     if i = 0#u32
     then
-      let back := fun ret => Result.ret (List.Cons ret tl)
-      Result.ret (x, back)
+      let back := fun ret => Result.ok (List.Cons ret tl)
+      Result.ok (x, back)
     else
       do
       let i1 ← i - 1#u32
@@ -246,8 +246,8 @@ divergent def list_nth_mut_loop_with_id_loop
       let back1 :=
         fun ret => do
                    let tl1 ← back ret
-                   Result.ret (List.Cons x tl1)
-      Result.ret (t, back1)
+                   Result.ok (List.Cons x tl1)
+      Result.ok (t, back1)
   | List.Nil => Result.fail .panic
 
 /- [loops::list_nth_mut_loop_with_id]:
@@ -260,7 +260,7 @@ def list_nth_mut_loop_with_id
   let back1 := fun ret => do
                           let l ← back ret
                           id_mut_back l
-  Result.ret (t, back1)
+  Result.ok (t, back1)
 
 /- [loops::list_nth_shared_loop_with_id]: loop 0:
    Source: 'src/loops.rs', lines 168:0-179:1 -/
@@ -269,7 +269,7 @@ divergent def list_nth_shared_loop_with_id_loop
   match ls with
   | List.Cons x tl =>
     if i = 0#u32
-    then Result.ret x
+    then Result.ok x
     else do
          let i1 ← i - 1#u32
          list_nth_shared_loop_with_id_loop T i1 tl
@@ -295,22 +295,22 @@ divergent def list_nth_mut_loop_pair_loop
     | List.Cons x1 tl1 =>
       if i = 0#u32
       then
-        let back_'a := fun ret => Result.ret (List.Cons ret tl0)
-        let back_'b := fun ret => Result.ret (List.Cons ret tl1)
-        Result.ret ((x0, x1), back_'a, back_'b)
+        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 - 1#u32
-        let (p, back_'a, back_'b) ← list_nth_mut_loop_pair_loop T tl0 tl1 i1
-        let back_'a1 :=
+        let (p, back'a, back'b) ← list_nth_mut_loop_pair_loop T tl0 tl1 i1
+        let back'a1 :=
           fun ret => do
-                     let tl01 ← back_'a ret
-                     Result.ret (List.Cons x0 tl01)
-        let back_'b1 :=
+                     let tl01 ← back'a ret
+                     Result.ok (List.Cons x0 tl01)
+        let back'b1 :=
           fun ret => do
-                     let tl11 ← back_'b ret
-                     Result.ret (List.Cons x1 tl11)
-        Result.ret (p, back_'a1, back_'b1)
+                     let tl11 ← back'b ret
+                     Result.ok (List.Cons x1 tl11)
+        Result.ok (p, back'a1, back'b1)
     | List.Nil => Result.fail .panic
   | List.Nil => Result.fail .panic
 
@@ -331,7 +331,7 @@ divergent def list_nth_shared_loop_pair_loop
     match ls1 with
     | List.Cons x1 tl1 =>
       if i = 0#u32
-      then Result.ret (x0, x1)
+      then Result.ok (x0, x1)
       else do
            let i1 ← i - 1#u32
            list_nth_shared_loop_pair_loop T tl0 tl1 i1
@@ -356,21 +356,21 @@ divergent def list_nth_mut_loop_pair_merge_loop
     | List.Cons x1 tl1 =>
       if i = 0#u32
       then
-        let back_'a :=
+        let back :=
           fun ret =>
             let (t, t1) := ret
-            Result.ret (List.Cons t tl0, List.Cons t1 tl1)
-        Result.ret ((x0, x1), back_'a)
+            Result.ok (List.Cons t tl0, List.Cons t1 tl1)
+        Result.ok ((x0, x1), back)
       else
         do
         let i1 ← i - 1#u32
-        let (p, back_'a) ← list_nth_mut_loop_pair_merge_loop T tl0 tl1 i1
-        let back_'a1 :=
+        let (p, back) ← list_nth_mut_loop_pair_merge_loop T tl0 tl1 i1
+        let back1 :=
           fun ret =>
             do
-            let (tl01, tl11) ← back_'a ret
-            Result.ret (List.Cons x0 tl01, List.Cons x1 tl11)
-        Result.ret (p, back_'a1)
+            let (tl01, tl11) ← back ret
+            Result.ok (List.Cons x0 tl01, List.Cons x1 tl11)
+        Result.ok (p, back1)
     | List.Nil => Result.fail .panic
   | List.Nil => Result.fail .panic
 
@@ -391,7 +391,7 @@ divergent def list_nth_shared_loop_pair_merge_loop
     match ls1 with
     | List.Cons x1 tl1 =>
       if i = 0#u32
-      then Result.ret (x0, x1)
+      then Result.ok (x0, x1)
       else
         do
         let i1 ← i - 1#u32
@@ -417,17 +417,17 @@ divergent def list_nth_mut_shared_loop_pair_loop
     | List.Cons x1 tl1 =>
       if i = 0#u32
       then
-        let back_'a := fun ret => Result.ret (List.Cons ret tl0)
-        Result.ret ((x0, x1), back_'a)
+        let back := fun ret => Result.ok (List.Cons ret tl0)
+        Result.ok ((x0, x1), back)
       else
         do
         let i1 ← i - 1#u32
-        let (p, back_'a) ← list_nth_mut_shared_loop_pair_loop T tl0 tl1 i1
-        let back_'a1 :=
+        let (p, back) ← list_nth_mut_shared_loop_pair_loop T tl0 tl1 i1
+        let back1 :=
           fun ret => do
-                     let tl01 ← back_'a ret
-                     Result.ret (List.Cons x0 tl01)
-        Result.ret (p, back_'a1)
+                     let tl01 ← back ret
+                     Result.ok (List.Cons x0 tl01)
+        Result.ok (p, back1)
     | List.Nil => Result.fail .panic
   | List.Nil => Result.fail .panic
 
@@ -451,18 +451,17 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop
     | List.Cons x1 tl1 =>
       if i = 0#u32
       then
-        let back_'a := fun ret => Result.ret (List.Cons ret tl0)
-        Result.ret ((x0, x1), back_'a)
+        let back := fun ret => Result.ok (List.Cons ret tl0)
+        Result.ok ((x0, x1), back)
       else
         do
         let i1 ← i - 1#u32
-        let (p, back_'a) ←
-          list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i1
-        let back_'a1 :=
+        let (p, back) ← list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i1
+        let back1 :=
           fun ret => do
-                     let tl01 ← back_'a ret
-                     Result.ret (List.Cons x0 tl01)
-        Result.ret (p, back_'a1)
+                     let tl01 ← back ret
+                     Result.ok (List.Cons x0 tl01)
+        Result.ok (p, back1)
     | List.Nil => Result.fail .panic
   | List.Nil => Result.fail .panic
 
@@ -486,17 +485,17 @@ divergent def list_nth_shared_mut_loop_pair_loop
     | List.Cons x1 tl1 =>
       if i = 0#u32
       then
-        let back_'b := fun ret => Result.ret (List.Cons ret tl1)
-        Result.ret ((x0, x1), back_'b)
+        let back := fun ret => Result.ok (List.Cons ret tl1)
+        Result.ok ((x0, x1), back)
       else
         do
         let i1 ← i - 1#u32
-        let (p, back_'b) ← list_nth_shared_mut_loop_pair_loop T tl0 tl1 i1
-        let back_'b1 :=
+        let (p, back) ← list_nth_shared_mut_loop_pair_loop T tl0 tl1 i1
+        let back1 :=
           fun ret => do
-                     let tl11 ← back_'b ret
-                     Result.ret (List.Cons x1 tl11)
-        Result.ret (p, back_'b1)
+                     let tl11 ← back ret
+                     Result.ok (List.Cons x1 tl11)
+        Result.ok (p, back1)
     | List.Nil => Result.fail .panic
   | List.Nil => Result.fail .panic
 
@@ -520,18 +519,17 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop
     | List.Cons x1 tl1 =>
       if i = 0#u32
       then
-        let back_'a := fun ret => Result.ret (List.Cons ret tl1)
-        Result.ret ((x0, x1), back_'a)
+        let back := fun ret => Result.ok (List.Cons ret tl1)
+        Result.ok ((x0, x1), back)
       else
         do
         let i1 ← i - 1#u32
-        let (p, back_'a) ←
-          list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i1
-        let back_'a1 :=
+        let (p, back) ← list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i1
+        let back1 :=
           fun ret => do
-                     let tl11 ← back_'a ret
-                     Result.ret (List.Cons x1 tl11)
-        Result.ret (p, back_'a1)
+                     let tl11 ← back ret
+                     Result.ok (List.Cons x1 tl11)
+        Result.ok (p, back1)
     | List.Nil => Result.fail .panic
   | List.Nil => Result.fail .panic
 
@@ -550,14 +548,14 @@ divergent def ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
   then do
        let i1 ← i - 1#u32
        ignore_input_mut_borrow_loop i1
-  else Result.ret ()
+  else Result.ok ()
 
 /- [loops::ignore_input_mut_borrow]:
    Source: 'src/loops.rs', lines 345:0-345:56 -/
 def ignore_input_mut_borrow (_a : U32) (i : U32) : Result U32 :=
   do
   let _ ← ignore_input_mut_borrow_loop i
-  Result.ret _a
+  Result.ok _a
 
 /- [loops::incr_ignore_input_mut_borrow]: loop 0:
    Source: 'src/loops.rs', lines 353:0-358:1 -/
@@ -566,7 +564,7 @@ divergent def incr_ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
   then do
        let i1 ← i - 1#u32
        incr_ignore_input_mut_borrow_loop i1
-  else Result.ret ()
+  else Result.ok ()
 
 /- [loops::incr_ignore_input_mut_borrow]:
    Source: 'src/loops.rs', lines 353:0-353:60 -/
@@ -574,7 +572,7 @@ def incr_ignore_input_mut_borrow (a : U32) (i : U32) : Result U32 :=
   do
   let a1 ← a + 1#u32
   let _ ← incr_ignore_input_mut_borrow_loop i
-  Result.ret a1
+  Result.ok a1
 
 /- [loops::ignore_input_shared_borrow]: loop 0:
    Source: 'src/loops.rs', lines 362:0-366:1 -/
@@ -583,13 +581,13 @@ divergent def ignore_input_shared_borrow_loop (i : U32) : Result Unit :=
   then do
        let i1 ← i - 1#u32
        ignore_input_shared_borrow_loop i1
-  else Result.ret ()
+  else Result.ok ()
 
 /- [loops::ignore_input_shared_borrow]:
    Source: 'src/loops.rs', lines 362:0-362:59 -/
 def ignore_input_shared_borrow (_a : U32) (i : U32) : Result U32 :=
   do
   let _ ← ignore_input_shared_borrow_loop i
-  Result.ret _a
+  Result.ok _a
 
 end loops
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 5f9ec0f2..7d28f7f9 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -159,24 +159,24 @@ def cast_bool_to_i32 (x : Bool) : Result I32 :=
 /- [no_nested_borrows::cast_bool_to_bool]:
    Source: 'src/no_nested_borrows.rs', lines 137:0-137:41 -/
 def cast_bool_to_bool (x : Bool) : Result Bool :=
-  Result.ret x
+  Result.ok x
 
 /- [no_nested_borrows::test2]:
    Source: 'src/no_nested_borrows.rs', lines 142:0-142:14 -/
 def test2 : Result Unit :=
   do
   let _ ← 23#u32 + 44#u32
-  Result.ret ()
+  Result.ok ()
 
 /- Unit test for [no_nested_borrows::test2] -/
-#assert (test2 == Result.ret ())
+#assert (test2 == Result.ok ())
 
 /- [no_nested_borrows::get_max]:
    Source: 'src/no_nested_borrows.rs', lines 154:0-154:37 -/
 def get_max (x : U32) (y : U32) : Result U32 :=
   if x >= y
-  then Result.ret x
-  else Result.ret y
+  then Result.ok x
+  else Result.ok y
 
 /- [no_nested_borrows::test3]:
    Source: 'src/no_nested_borrows.rs', lines 162:0-162:14 -/
@@ -187,10 +187,10 @@ def test3 : Result Unit :=
   let z ← x + y
   if ¬ (z = 15#u32)
   then Result.fail .panic
-  else Result.ret ()
+  else Result.ok ()
 
 /- Unit test for [no_nested_borrows::test3] -/
-#assert (test3 == Result.ret ())
+#assert (test3 == Result.ok ())
 
 /- [no_nested_borrows::test_neg1]:
    Source: 'src/no_nested_borrows.rs', lines 169:0-169:18 -/
@@ -199,20 +199,20 @@ def test_neg1 : Result Unit :=
   let y ← -. 3#i32
   if ¬ (y = (-3)#i32)
   then Result.fail .panic
-  else Result.ret ()
+  else Result.ok ()
 
 /- Unit test for [no_nested_borrows::test_neg1] -/
-#assert (test_neg1 == Result.ret ())
+#assert (test_neg1 == Result.ok ())
 
 /- [no_nested_borrows::refs_test1]:
    Source: 'src/no_nested_borrows.rs', lines 176:0-176:19 -/
 def refs_test1 : Result Unit :=
   if ¬ (1#i32 = 1#i32)
   then Result.fail .panic
-  else Result.ret ()
+  else Result.ok ()
 
 /- Unit test for [no_nested_borrows::refs_test1] -/
-#assert (refs_test1 == Result.ret ())
+#assert (refs_test1 == Result.ok ())
 
 /- [no_nested_borrows::refs_test2]:
    Source: 'src/no_nested_borrows.rs', lines 187:0-187:19 -/
@@ -227,18 +227,18 @@ def refs_test2 : Result Unit :=
       then Result.fail .panic
       else if ¬ (2#i32 = 2#i32)
            then Result.fail .panic
-           else Result.ret ()
+           else Result.ok ()
 
 /- Unit test for [no_nested_borrows::refs_test2] -/
-#assert (refs_test2 == Result.ret ())
+#assert (refs_test2 == Result.ok ())
 
 /- [no_nested_borrows::test_list1]:
    Source: 'src/no_nested_borrows.rs', lines 203:0-203:19 -/
 def test_list1 : Result Unit :=
-  Result.ret ()
+  Result.ok ()
 
 /- Unit test for [no_nested_borrows::test_list1] -/
-#assert (test_list1 == Result.ret ())
+#assert (test_list1 == Result.ok ())
 
 /- [no_nested_borrows::test_box1]:
    Source: 'src/no_nested_borrows.rs', lines 208:0-208:18 -/
@@ -249,29 +249,29 @@ def test_box1 : Result Unit :=
   let x ← alloc.boxed.Box.deref I32 b
   if ¬ (x = 1#i32)
   then Result.fail .panic
-  else Result.ret ()
+  else Result.ok ()
 
 /- Unit test for [no_nested_borrows::test_box1] -/
-#assert (test_box1 == Result.ret ())
+#assert (test_box1 == Result.ok ())
 
 /- [no_nested_borrows::copy_int]:
    Source: 'src/no_nested_borrows.rs', lines 218:0-218:30 -/
 def copy_int (x : I32) : Result I32 :=
-  Result.ret x
+  Result.ok x
 
 /- [no_nested_borrows::test_unreachable]:
    Source: 'src/no_nested_borrows.rs', lines 224:0-224:32 -/
 def test_unreachable (b : Bool) : Result Unit :=
   if b
   then Result.fail .panic
-  else Result.ret ()
+  else Result.ok ()
 
 /- [no_nested_borrows::test_panic]:
    Source: 'src/no_nested_borrows.rs', lines 232:0-232:26 -/
 def test_panic (b : Bool) : Result Unit :=
   if b
   then Result.fail .panic
-  else Result.ret ()
+  else Result.ok ()
 
 /- [no_nested_borrows::test_copy_int]:
    Source: 'src/no_nested_borrows.rs', lines 239:0-239:22 -/
@@ -280,17 +280,17 @@ def test_copy_int : Result Unit :=
   let y ← copy_int 0#i32
   if ¬ (0#i32 = y)
   then Result.fail .panic
-  else Result.ret ()
+  else Result.ok ()
 
 /- Unit test for [no_nested_borrows::test_copy_int] -/
-#assert (test_copy_int == Result.ret ())
+#assert (test_copy_int == Result.ok ())
 
 /- [no_nested_borrows::is_cons]:
    Source: 'src/no_nested_borrows.rs', lines 246:0-246:38 -/
 def is_cons (T : Type) (l : List T) : Result Bool :=
   match l with
-  | List.Cons _ _ => Result.ret true
-  | List.Nil => Result.ret false
+  | List.Cons _ _ => Result.ok true
+  | List.Nil => Result.ok false
 
 /- [no_nested_borrows::test_is_cons]:
    Source: 'src/no_nested_borrows.rs', lines 253:0-253:21 -/
@@ -299,16 +299,16 @@ def test_is_cons : Result Unit :=
   let b ← is_cons I32 (List.Cons 0#i32 List.Nil)
   if ¬ b
   then Result.fail .panic
-  else Result.ret ()
+  else Result.ok ()
 
 /- Unit test for [no_nested_borrows::test_is_cons] -/
-#assert (test_is_cons == Result.ret ())
+#assert (test_is_cons == Result.ok ())
 
 /- [no_nested_borrows::split_list]:
    Source: 'src/no_nested_borrows.rs', lines 259:0-259:48 -/
 def split_list (T : Type) (l : List T) : Result (T × (List T)) :=
   match l with
-  | List.Cons hd tl => Result.ret (hd, tl)
+  | List.Cons hd tl => Result.ok (hd, tl)
   | List.Nil => Result.fail .panic
 
 /- [no_nested_borrows::test_split_list]:
@@ -319,10 +319,10 @@ def test_split_list : Result Unit :=
   let (hd, _) := p
   if ¬ (hd = 0#i32)
   then Result.fail .panic
-  else Result.ret ()
+  else Result.ok ()
 
 /- Unit test for [no_nested_borrows::test_split_list] -/
-#assert (test_split_list == Result.ret ())
+#assert (test_split_list == Result.ok ())
 
 /- [no_nested_borrows::choose]:
    Source: 'src/no_nested_borrows.rs', lines 274:0-274:70 -/
@@ -331,10 +331,10 @@ def choose
   Result (T × (T → Result (T × T)))
   :=
   if b
-  then let back_'a := fun ret => Result.ret (ret, y)
-       Result.ret (x, back_'a)
-  else let back_'a := fun ret => Result.ret (x, ret)
-       Result.ret (y, back_'a)
+  then let back := fun ret => Result.ok (ret, y)
+       Result.ok (x, back)
+  else let back := fun ret => Result.ok (x, ret)
+       Result.ok (y, back)
 
 /- [no_nested_borrows::choose_test]:
    Source: 'src/no_nested_borrows.rs', lines 282:0-282:20 -/
@@ -351,15 +351,15 @@ def choose_test : Result Unit :=
     then Result.fail .panic
     else if ¬ (y = 0#i32)
          then Result.fail .panic
-         else Result.ret ()
+         else Result.ok ()
 
 /- Unit test for [no_nested_borrows::choose_test] -/
-#assert (choose_test == Result.ret ())
+#assert (choose_test == Result.ok ())
 
 /- [no_nested_borrows::test_char]:
    Source: 'src/no_nested_borrows.rs', lines 294:0-294:26 -/
 def test_char : Result Char :=
-  Result.ret 'a'
+  Result.ok 'a'
 
 mutual
 
@@ -384,7 +384,7 @@ divergent def list_length (T : Type) (l : List T) : Result U32 :=
   | List.Cons _ l1 => do
                       let i ← list_length T l1
                       1#u32 + i
-  | List.Nil => Result.ret 0#u32
+  | List.Nil => Result.ok 0#u32
 
 /- [no_nested_borrows::list_nth_shared]:
    Source: 'src/no_nested_borrows.rs', lines 347:0-347:62 -/
@@ -392,7 +392,7 @@ divergent def list_nth_shared (T : Type) (l : List T) (i : U32) : Result T :=
   match l with
   | List.Cons x tl =>
     if i = 0#u32
-    then Result.ret x
+    then Result.ok x
     else do
          let i1 ← i - 1#u32
          list_nth_shared T tl i1
@@ -406,18 +406,18 @@ divergent def list_nth_mut
   | List.Cons x tl =>
     if i = 0#u32
     then
-      let back_'a := fun ret => Result.ret (List.Cons ret tl)
-      Result.ret (x, back_'a)
+      let back := fun ret => Result.ok (List.Cons ret tl)
+      Result.ok (x, back)
     else
       do
       let i1 ← i - 1#u32
       let (t, list_nth_mut_back) ← list_nth_mut T tl i1
-      let back_'a :=
+      let back :=
         fun ret =>
           do
           let tl1 ← list_nth_mut_back ret
-          Result.ret (List.Cons x tl1)
-      Result.ret (t, back_'a)
+          Result.ok (List.Cons x tl1)
+      Result.ok (t, back)
   | List.Nil => Result.fail .panic
 
 /- [no_nested_borrows::list_rev_aux]:
@@ -426,7 +426,7 @@ divergent def list_rev_aux
   (T : Type) (li : List T) (lo : List T) : Result (List T) :=
   match li with
   | List.Cons hd tl => list_rev_aux T tl (List.Cons hd lo)
-  | List.Nil => Result.ret lo
+  | List.Nil => Result.ok lo
 
 /- [no_nested_borrows::list_rev]:
    Source: 'src/no_nested_borrows.rs', lines 393:0-393:42 -/
@@ -476,10 +476,10 @@ def test_list_functions : Result Unit :=
               let i6 ← list_nth_shared I32 ls 2#u32
               if ¬ (i6 = 2#i32)
               then Result.fail .panic
-              else Result.ret ()
+              else Result.ok ()
 
 /- Unit test for [no_nested_borrows::test_list_functions] -/
-#assert (test_list_functions == Result.ret ())
+#assert (test_list_functions == Result.ok ())
 
 /- [no_nested_borrows::id_mut_pair1]:
    Source: 'src/no_nested_borrows.rs', lines 414:0-414:89 -/
@@ -487,7 +487,7 @@ def id_mut_pair1
   (T1 T2 : Type) (x : T1) (y : T2) :
   Result ((T1 × T2) × ((T1 × T2) → Result (T1 × T2)))
   :=
-  Result.ret ((x, y), Result.ret)
+  Result.ok ((x, y), Result.ok)
 
 /- [no_nested_borrows::id_mut_pair2]:
    Source: 'src/no_nested_borrows.rs', lines 418:0-418:88 -/
@@ -496,7 +496,7 @@ def id_mut_pair2
   Result ((T1 × T2) × ((T1 × T2) → Result (T1 × T2)))
   :=
   let (t, t1) := p
-  Result.ret ((t, t1), Result.ret)
+  Result.ok ((t, t1), Result.ok)
 
 /- [no_nested_borrows::id_mut_pair3]:
    Source: 'src/no_nested_borrows.rs', lines 422:0-422:93 -/
@@ -504,7 +504,7 @@ def id_mut_pair3
   (T1 T2 : Type) (x : T1) (y : T2) :
   Result ((T1 × T2) × (T1 → Result T1) × (T2 → Result T2))
   :=
-  Result.ret ((x, y), Result.ret, Result.ret)
+  Result.ok ((x, y), Result.ok, Result.ok)
 
 /- [no_nested_borrows::id_mut_pair4]:
    Source: 'src/no_nested_borrows.rs', lines 426:0-426:92 -/
@@ -513,7 +513,7 @@ def id_mut_pair4
   Result ((T1 × T2) × (T1 → Result T1) × (T2 → Result T2))
   :=
   let (t, t1) := p
-  Result.ret ((t, t1), Result.ret, Result.ret)
+  Result.ok ((t, t1), Result.ok, Result.ok)
 
 /- [no_nested_borrows::StructWithTuple]
    Source: 'src/no_nested_borrows.rs', lines 433:0-433:34 -/
@@ -523,17 +523,17 @@ structure StructWithTuple (T1 T2 : Type) where
 /- [no_nested_borrows::new_tuple1]:
    Source: 'src/no_nested_borrows.rs', lines 437:0-437:48 -/
 def new_tuple1 : Result (StructWithTuple U32 U32) :=
-  Result.ret { p := (1#u32, 2#u32) }
+  Result.ok { p := (1#u32, 2#u32) }
 
 /- [no_nested_borrows::new_tuple2]:
    Source: 'src/no_nested_borrows.rs', lines 441:0-441:48 -/
 def new_tuple2 : Result (StructWithTuple I16 I16) :=
-  Result.ret { p := (1#i16, 2#i16) }
+  Result.ok { p := (1#i16, 2#i16) }
 
 /- [no_nested_borrows::new_tuple3]:
    Source: 'src/no_nested_borrows.rs', lines 445:0-445:48 -/
 def new_tuple3 : Result (StructWithTuple U64 I64) :=
-  Result.ret { p := (1#u64, 2#i64) }
+  Result.ok { p := (1#u64, 2#i64) }
 
 /- [no_nested_borrows::StructWithPair]
    Source: 'src/no_nested_borrows.rs', lines 450:0-450:33 -/
@@ -543,7 +543,7 @@ structure StructWithPair (T1 T2 : Type) where
 /- [no_nested_borrows::new_pair1]:
    Source: 'src/no_nested_borrows.rs', lines 454:0-454:46 -/
 def new_pair1 : Result (StructWithPair U32 U32) :=
-  Result.ret { p := { x := 1#u32, y := 2#u32 } }
+  Result.ok { p := { x := 1#u32, y := 2#u32 } }
 
 /- [no_nested_borrows::test_constants]:
    Source: 'src/no_nested_borrows.rs', lines 462:0-462:23 -/
@@ -570,18 +570,18 @@ def test_constants : Result Unit :=
         let swp ← new_pair1
         if ¬ (swp.p.x = 1#u32)
         then Result.fail .panic
-        else Result.ret ()
+        else Result.ok ()
 
 /- Unit test for [no_nested_borrows::test_constants] -/
-#assert (test_constants == Result.ret ())
+#assert (test_constants == Result.ok ())
 
 /- [no_nested_borrows::test_weird_borrows1]:
    Source: 'src/no_nested_borrows.rs', lines 471:0-471:28 -/
 def test_weird_borrows1 : Result Unit :=
-  Result.ret ()
+  Result.ok ()
 
 /- Unit test for [no_nested_borrows::test_weird_borrows1] -/
-#assert (test_weird_borrows1 == Result.ret ())
+#assert (test_weird_borrows1 == Result.ok ())
 
 /- [no_nested_borrows::test_mem_replace]:
    Source: 'src/no_nested_borrows.rs', lines 481:0-481:37 -/
@@ -589,31 +589,31 @@ def test_mem_replace (px : U32) : Result U32 :=
   let (y, _) := core.mem.replace U32 px 1#u32
   if ¬ (y = 0#u32)
   then Result.fail .panic
-  else Result.ret 2#u32
+  else Result.ok 2#u32
 
 /- [no_nested_borrows::test_shared_borrow_bool1]:
    Source: 'src/no_nested_borrows.rs', lines 488:0-488:47 -/
 def test_shared_borrow_bool1 (b : Bool) : Result U32 :=
   if b
-  then Result.ret 0#u32
-  else Result.ret 1#u32
+  then Result.ok 0#u32
+  else Result.ok 1#u32
 
 /- [no_nested_borrows::test_shared_borrow_bool2]:
    Source: 'src/no_nested_borrows.rs', lines 501:0-501:40 -/
 def test_shared_borrow_bool2 : Result U32 :=
-  Result.ret 0#u32
+  Result.ok 0#u32
 
 /- [no_nested_borrows::test_shared_borrow_enum1]:
    Source: 'src/no_nested_borrows.rs', lines 516:0-516:52 -/
 def test_shared_borrow_enum1 (l : List U32) : Result U32 :=
   match l with
-  | List.Cons _ _ => Result.ret 1#u32
-  | List.Nil => Result.ret 0#u32
+  | List.Cons _ _ => Result.ok 1#u32
+  | List.Nil => Result.ok 0#u32
 
 /- [no_nested_borrows::test_shared_borrow_enum2]:
    Source: 'src/no_nested_borrows.rs', lines 528:0-528:40 -/
 def test_shared_borrow_enum2 : Result U32 :=
-  Result.ret 0#u32
+  Result.ok 0#u32
 
 /- [no_nested_borrows::incr]:
    Source: 'src/no_nested_borrows.rs', lines 539:0-539:24 -/
@@ -630,7 +630,7 @@ def call_incr (x : U32) : Result U32 :=
 def read_then_incr (x : U32) : Result (U32 × U32) :=
   do
   let x1 ← x + 1#u32
-  Result.ret (x, x1)
+  Result.ok (x, x1)
 
 /- [no_nested_borrows::Tuple]
    Source: 'src/no_nested_borrows.rs', lines 554:0-554:24 -/
@@ -639,12 +639,12 @@ def Tuple (T1 T2 : Type) := T1 × T2
 /- [no_nested_borrows::use_tuple_struct]:
    Source: 'src/no_nested_borrows.rs', lines 556:0-556:48 -/
 def use_tuple_struct (x : Tuple U32 U32) : Result (Tuple U32 U32) :=
-  Result.ret (1#u32, x.#1)
+  Result.ok (1#u32, x.#1)
 
 /- [no_nested_borrows::create_tuple_struct]:
    Source: 'src/no_nested_borrows.rs', lines 560:0-560:61 -/
 def create_tuple_struct (x : U32) (y : U64) : Result (Tuple U32 U64) :=
-  Result.ret (x, y)
+  Result.ok (x, y)
 
 /- [no_nested_borrows::IdType]
    Source: 'src/no_nested_borrows.rs', lines 565:0-565:20 -/
@@ -653,11 +653,11 @@ def create_tuple_struct (x : U32) (y : U64) : Result (Tuple U32 U64) :=
 /- [no_nested_borrows::use_id_type]:
    Source: 'src/no_nested_borrows.rs', lines 567:0-567:40 -/
 def use_id_type (T : Type) (x : IdType T) : Result T :=
-  Result.ret x
+  Result.ok x
 
 /- [no_nested_borrows::create_id_type]:
    Source: 'src/no_nested_borrows.rs', lines 571:0-571:43 -/
 def create_id_type (T : Type) (x : T) : Result (IdType T) :=
-  Result.ret x
+  Result.ok x
 
 end no_nested_borrows
diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
index 924ff36c..32203eca 100644
--- a/tests/lean/Paper.lean
+++ b/tests/lean/Paper.lean
@@ -17,10 +17,10 @@ def test_incr : Result Unit :=
   let x ← ref_incr 0#i32
   if ¬ (x = 1#i32)
   then Result.fail .panic
-  else Result.ret ()
+  else Result.ok ()
 
 /- Unit test for [paper::test_incr] -/
-#assert (test_incr == Result.ret ())
+#assert (test_incr == Result.ok ())
 
 /- [paper::choose]:
    Source: 'src/paper.rs', lines 15:0-15:70 -/
@@ -29,10 +29,10 @@ def choose
   Result (T × (T → Result (T × T)))
   :=
   if b
-  then let back_'a := fun ret => Result.ret (ret, y)
-       Result.ret (x, back_'a)
-  else let back_'a := fun ret => Result.ret (x, ret)
-       Result.ret (y, back_'a)
+  then let back := fun ret => Result.ok (ret, y)
+       Result.ok (x, back)
+  else let back := fun ret => Result.ok (x, ret)
+       Result.ok (y, back)
 
 /- [paper::test_choose]:
    Source: 'src/paper.rs', lines 23:0-23:20 -/
@@ -49,10 +49,10 @@ def test_choose : Result Unit :=
     then Result.fail .panic
     else if ¬ (y = 0#i32)
          then Result.fail .panic
-         else Result.ret ()
+         else Result.ok ()
 
 /- Unit test for [paper::test_choose] -/
-#assert (test_choose == Result.ret ())
+#assert (test_choose == Result.ok ())
 
 /- [paper::List]
    Source: 'src/paper.rs', lines 35:0-35:16 -/
@@ -68,18 +68,18 @@ divergent def list_nth_mut
   | List.Cons x tl =>
     if i = 0#u32
     then
-      let back_'a := fun ret => Result.ret (List.Cons ret tl)
-      Result.ret (x, back_'a)
+      let back := fun ret => Result.ok (List.Cons ret tl)
+      Result.ok (x, back)
     else
       do
       let i1 ← i - 1#u32
       let (t, list_nth_mut_back) ← list_nth_mut T tl i1
-      let back_'a :=
+      let back :=
         fun ret =>
           do
           let tl1 ← list_nth_mut_back ret
-          Result.ret (List.Cons x tl1)
-      Result.ret (t, back_'a)
+          Result.ok (List.Cons x tl1)
+      Result.ok (t, back)
   | List.Nil => Result.fail .panic
 
 /- [paper::sum]:
@@ -89,7 +89,7 @@ divergent def sum (l : List I32) : Result I32 :=
   | List.Cons x tl => do
                       let i ← sum tl
                       x + i
-  | List.Nil => Result.ret 0#i32
+  | List.Nil => Result.ok 0#i32
 
 /- [paper::test_nth]:
    Source: 'src/paper.rs', lines 68:0-68:17 -/
@@ -103,10 +103,10 @@ def test_nth : Result Unit :=
   let i ← sum l2
   if ¬ (i = 7#i32)
   then Result.fail .panic
-  else Result.ret ()
+  else Result.ok ()
 
 /- Unit test for [paper::test_nth] -/
-#assert (test_nth == Result.ret ())
+#assert (test_nth == Result.ok ())
 
 /- [paper::call_choose]:
    Source: 'src/paper.rs', lines 76:0-76:44 -/
@@ -116,6 +116,6 @@ def call_choose (p : (U32 × U32)) : Result U32 :=
   let (pz, choose_back) ← choose U32 true px py
   let pz1 ← pz + 1#u32
   let (px1, _) ← choose_back pz1
-  Result.ret px1
+  Result.ok px1
 
 end paper
diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean
index 59c557a0..09f41056 100644
--- a/tests/lean/PoloniusList.lean
+++ b/tests/lean/PoloniusList.lean
@@ -20,16 +20,16 @@ divergent def get_list_at_x
   match ls with
   | List.Cons hd tl =>
     if hd = x
-    then Result.ret (List.Cons hd tl, Result.ret)
+    then Result.ok (List.Cons hd tl, Result.ok)
     else
       do
       let (l, get_list_at_x_back) ← get_list_at_x tl x
-      let back_'a :=
+      let back :=
         fun ret =>
           do
           let tl1 ← get_list_at_x_back ret
-          Result.ret (List.Cons hd tl1)
-      Result.ret (l, back_'a)
-  | List.Nil => Result.ret (List.Nil, Result.ret)
+          Result.ok (List.Cons hd tl1)
+      Result.ok (l, back)
+  | List.Nil => Result.ok (List.Nil, Result.ok)
 
 end polonius_list
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
index acddd1a9..0076e6f6 100644
--- a/tests/lean/Traits.lean
+++ b/tests/lean/Traits.lean
@@ -13,7 +13,7 @@ structure BoolTrait (Self : Type) where
 /- [traits::{(traits::BoolTrait for bool)}::get_bool]:
    Source: 'src/traits.rs', lines 12:4-12:30 -/
 def BoolTraitBool.get_bool (self : Bool) : Result Bool :=
-  Result.ret self
+  Result.ok self
 
 /- Trait implementation: [traits::{(traits::BoolTrait for bool)}]
    Source: 'src/traits.rs', lines 11:0-11:23 -/
@@ -25,7 +25,7 @@ def BoolTraitBool : BoolTrait Bool := {
    Source: 'src/traits.rs', lines 6:4-6:30 -/
 def BoolTrait.ret_true
   {Self : Type} (self_clause : BoolTrait Self) (self : Self) : Result Bool :=
-  Result.ret true
+  Result.ok true
 
 /- [traits::test_bool_trait_bool]:
    Source: 'src/traits.rs', lines 17:0-17:44 -/
@@ -34,14 +34,14 @@ def test_bool_trait_bool (x : Bool) : Result Bool :=
   let b ← BoolTraitBool.get_bool x
   if b
   then BoolTrait.ret_true BoolTraitBool x
-  else Result.ret false
+  else Result.ok false
 
 /- [traits::{(traits::BoolTrait for core::option::Option<T>)#1}::get_bool]:
    Source: 'src/traits.rs', lines 23:4-23:30 -/
 def BoolTraitOption.get_bool (T : Type) (self : Option T) : Result Bool :=
   match self with
-  | none => Result.ret false
-  | some _ => Result.ret true
+  | none => Result.ok false
+  | some _ => Result.ok true
 
 /- Trait implementation: [traits::{(traits::BoolTrait for core::option::Option<T>)#1}]
    Source: 'src/traits.rs', lines 22:0-22:31 -/
@@ -56,7 +56,7 @@ def test_bool_trait_option (T : Type) (x : Option T) : Result Bool :=
   let b ← BoolTraitOption.get_bool T x
   if b
   then BoolTrait.ret_true (BoolTraitOption T) x
-  else Result.ret false
+  else Result.ok false
 
 /- [traits::test_bool_trait]:
    Source: 'src/traits.rs', lines 35:0-35:50 -/
@@ -72,7 +72,7 @@ structure ToU64 (Self : Type) where
 /- [traits::{(traits::ToU64 for u64)#2}::to_u64]:
    Source: 'src/traits.rs', lines 44:4-44:26 -/
 def ToU64U64.to_u64 (self : U64) : Result U64 :=
-  Result.ret self
+  Result.ok self
 
 /- Trait implementation: [traits::{(traits::ToU64 for u64)#2}]
    Source: 'src/traits.rs', lines 43:0-43:18 -/
@@ -148,7 +148,7 @@ structure ToType (Self T : Type) where
 /- [traits::{(traits::ToType<bool> for u64)#5}::to_type]:
    Source: 'src/traits.rs', lines 93:4-93:28 -/
 def ToTypeU64Bool.to_type (self : U64) : Result Bool :=
-  Result.ret (self > 0#u64)
+  Result.ok (self > 0#u64)
 
 /- Trait implementation: [traits::{(traits::ToType<bool> for u64)#5}]
    Source: 'src/traits.rs', lines 92:0-92:25 -/
@@ -202,7 +202,7 @@ structure TestType.test.TestTrait (Self : Type) where
    Source: 'src/traits.rs', lines 139:12-139:34 -/
 def TestType.test.TestTraittraitsTestTypetestTestType1.test
   (self : TestType.test.TestType1) : Result Bool :=
-  Result.ret (self > 1#u64)
+  Result.ok (self > 1#u64)
 
 /- Trait implementation: [traits::{traits::TestType<T>#6}::test::{(traits::{traits::TestType<T>#6}::test::TestTrait for traits::{traits::TestType<T>#6}::test::TestType1)}]
    Source: 'src/traits.rs', lines 138:8-138:36 -/
@@ -219,7 +219,7 @@ def TestType.test
   let x1 ← ToU64Inst.to_u64 x
   if x1 > 0#u64
   then TestType.test.TestTraittraitsTestTypetestTestType1.test 0#u64
-  else Result.ret false
+  else Result.ok false
 
 /- [traits::BoolWrapper]
    Source: 'src/traits.rs', lines 150:0-150:22 -/
@@ -243,7 +243,7 @@ def ToTypetraitsBoolWrapperT (T : Type) (ToTypeBoolTInst : ToType Bool T) :
 /- [traits::WithConstTy::LEN2]
    Source: 'src/traits.rs', lines 164:4-164:21 -/
 def WithConstTy.LEN2_default_body (Self : Type) (LEN : Usize) : Result Usize :=
-  Result.ret 32#usize
+  Result.ok 32#usize
 def WithConstTy.LEN2_default (Self : Type) (LEN : Usize) : Usize :=
   eval_global (WithConstTy.LEN2_default_body Self LEN)
 
@@ -259,13 +259,13 @@ structure WithConstTy (Self : Type) (LEN : Usize) where
 
 /- [traits::{(traits::WithConstTy<32: usize> for bool)#8}::LEN1]
    Source: 'src/traits.rs', lines 175:4-175:21 -/
-def WithConstTyBool32.LEN1_body : Result Usize := Result.ret 12#usize
+def WithConstTyBool32.LEN1_body : Result Usize := Result.ok 12#usize
 def WithConstTyBool32.LEN1 : Usize := eval_global WithConstTyBool32.LEN1_body
 
 /- [traits::{(traits::WithConstTy<32: usize> for bool)#8}::f]:
    Source: 'src/traits.rs', lines 180:4-180:39 -/
 def WithConstTyBool32.f (i : U64) (a : Array U8 32#usize) : Result U64 :=
-  Result.ret i
+  Result.ok i
 
 /- Trait implementation: [traits::{(traits::WithConstTy<32: usize> for bool)#8}]
    Source: 'src/traits.rs', lines 174:0-174:29 -/
@@ -284,7 +284,7 @@ def use_with_const_ty1
   (H : Type) (LEN : Usize) (WithConstTyInst : WithConstTy H LEN) :
   Result Usize
   :=
-  Result.ret WithConstTyInst.LEN1
+  Result.ok WithConstTyInst.LEN1
 
 /- [traits::use_with_const_ty2]:
    Source: 'src/traits.rs', lines 187:0-187:73 -/
@@ -293,7 +293,7 @@ def use_with_const_ty2
   (w : WithConstTyInst.W) :
   Result Unit
   :=
-  Result.ret ()
+  Result.ok ()
 
 /- [traits::use_with_const_ty3]:
    Source: 'src/traits.rs', lines 189:0-189:80 -/
@@ -307,7 +307,7 @@ def use_with_const_ty3
 /- [traits::test_where1]:
    Source: 'src/traits.rs', lines 193:0-193:40 -/
 def test_where1 (T : Type) (_x : T) : Result Unit :=
-  Result.ret ()
+  Result.ok ()
 
 /- [traits::test_where2]:
    Source: 'src/traits.rs', lines 194:0-194:57 -/
@@ -315,7 +315,7 @@ def test_where2
   (T : Type) (WithConstTyT32Inst : WithConstTy T 32#usize) (_x : U32) :
   Result Unit
   :=
-  Result.ret ()
+  Result.ok ()
 
 /- Trait declaration: [traits::ParentTrait0]
    Source: 'src/traits.rs', lines 200:0-200:22 -/
@@ -355,7 +355,7 @@ def order1
   ParentTrait0 U) :
   Result Unit
   :=
-  Result.ret ()
+  Result.ok ()
 
 /- Trait declaration: [traits::ChildTrait1]
    Source: 'src/traits.rs', lines 222:0-222:35 -/
@@ -429,7 +429,7 @@ def ParentTrait2U32 : ParentTrait2 U32 := {
 /- [traits::{(traits::ChildTrait2 for u32)#13}::convert]:
    Source: 'src/traits.rs', lines 273:4-273:29 -/
 def ChildTrait2U32.convert (x : U32) : Result U32 :=
-  Result.ret x
+  Result.ok x
 
 /- Trait implementation: [traits::{(traits::ChildTrait2 for u32)#13}]
    Source: 'src/traits.rs', lines 272:0-272:24 -/
@@ -475,7 +475,7 @@ structure Trait (Self : Type) where
 
 /- [traits::{(traits::Trait for @Array<T, N>)#14}::LEN]
    Source: 'src/traits.rs', lines 315:4-315:20 -/
-def TraitArray.LEN_body (T : Type) (N : Usize) : Result Usize := Result.ret N
+def TraitArray.LEN_body (T : Type) (N : Usize) : Result Usize := Result.ok N
 def TraitArray.LEN (T : Type) (N : Usize) : Usize :=
   eval_global (TraitArray.LEN_body T N)
 
@@ -489,7 +489,7 @@ def TraitArray (T : Type) (N : Usize) : Trait (Array T N) := {
    Source: 'src/traits.rs', lines 319:4-319:20 -/
 def TraittraitsWrapper.LEN_body (T : Type) (TraitInst : Trait T)
   : Result Usize :=
-  Result.ret 0#usize
+  Result.ok 0#usize
 def TraittraitsWrapper.LEN (T : Type) (TraitInst : Trait T) : Usize :=
   eval_global (TraittraitsWrapper.LEN_body T TraitInst)
 
@@ -503,7 +503,7 @@ def TraittraitsWrapper (T : Type) (TraitInst : Trait T) : Trait (Wrapper T)
 /- [traits::use_wrapper_len]:
    Source: 'src/traits.rs', lines 322:0-322:43 -/
 def use_wrapper_len (T : Type) (TraitInst : Trait T) : Result Usize :=
-  Result.ret (TraittraitsWrapper T TraitInst).LEN
+  Result.ok (TraittraitsWrapper T TraitInst).LEN
 
 /- [traits::Foo]
    Source: 'src/traits.rs', lines 326:0-326:20 -/
@@ -512,7 +512,8 @@ structure Foo (T U : Type) where
   y : U
 
 /- [core::result::Result]
-   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21 -/
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21
+   Name pattern: core::result::Result -/
 inductive core.result.Result (T E : Type) :=
 | Ok : T → core.result.Result T E
 | Err : E → core.result.Result T E
@@ -521,7 +522,7 @@ inductive core.result.Result (T E : Type) :=
    Source: 'src/traits.rs', lines 332:4-332:33 -/
 def Foo.FOO_body (T U : Type) (TraitInst : Trait T)
   : Result (core.result.Result T I32) :=
-  Result.ret (core.result.Result.Err 0#i32)
+  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)
 
@@ -529,12 +530,12 @@ def Foo.FOO (T U : Type) (TraitInst : Trait T) : core.result.Result T I32 :=
    Source: 'src/traits.rs', lines 335:0-335:48 -/
 def use_foo1
   (T U : Type) (TraitInst : Trait T) : Result (core.result.Result T I32) :=
-  Result.ret (Foo.FOO T U TraitInst)
+  Result.ok (Foo.FOO T U TraitInst)
 
 /- [traits::use_foo2]:
    Source: 'src/traits.rs', lines 339:0-339:48 -/
 def use_foo2
   (T U : Type) (TraitInst : Trait U) : Result (core.result.Result U I32) :=
-  Result.ret (Foo.FOO U T TraitInst)
+  Result.ok (Foo.FOO U T TraitInst)
 
 end traits
diff --git a/tests/lean/Tutorial.lean b/tests/lean/Tutorial.lean
index d92b2dd7..94b70991 100644
--- a/tests/lean/Tutorial.lean
+++ b/tests/lean/Tutorial.lean
@@ -18,7 +18,7 @@ namespace Tutorial
 def mul2_add1 (x : U32) : Result U32 := do
   let x1 ← x + x
   let x2 ← x1 + 1#u32
-  ret x2
+  ok x2
 
 /- There are several things to note.
 
@@ -75,9 +75,9 @@ def mul2_add1 (x : U32) : Result U32 := do
  -/
 def mul2_add1_desugared (x : U32) : Result U32 :=
   match Scalar.add x x with
-  | ret x1 => -- Success case
+  | ok x1 => -- Success case
     match Scalar.add x1 (U32.ofInt 1) with
-    | ret x2 => ret x2
+    | ok x2 => ok x2
     | error => error
   | error => error -- Propagating the errors
 
@@ -105,7 +105,7 @@ theorem mul2_add1_spec
    -/
   (h : 2 * ↑x + 1 ≤ U32.max)
   /- The postcondition -/
-  : ∃ y, mul2_add1 x = ret y ∧  -- The call succeeds
+  : ∃ y, mul2_add1 x = ok y ∧  -- The call succeeds
   ↑ y = 2 * ↑x + (1 : Int)   -- The output has the expected value
   := by
   /- The proof -/
@@ -154,7 +154,7 @@ theorem mul2_add1_spec
  -/
 @[pspec] -- the [pspec] attribute saves the theorem in a database, for [progress] to use it
 theorem mul2_add1_spec2 (x : U32) (h : 2 * ↑x + 1 ≤ U32.max)
-  : ∃ y, mul2_add1 x = ret y ∧
+  : ∃ y, mul2_add1 x = ok y ∧
   ↑ y = 2 * ↑x + (1 : Int)
   := by
   rw [mul2_add1]
@@ -172,7 +172,7 @@ def use_mul2_add1 (x : U32) (y : U32) : Result U32 := do
 
 @[pspec]
 theorem use_mul2_add1_spec (x : U32) (y : U32) (h : 2 * ↑x + 1 + ↑y ≤ U32.max) :
-  ∃ z, use_mul2_add1 x y = ret z ∧
+  ∃ z, use_mul2_add1 x y = ok z ∧
   ↑z = 2 * ↑x + (1 : Int) + ↑y := by
   rw [use_mul2_add1]
   -- Here we use [progress] on [mul2_add1]
@@ -230,7 +230,7 @@ divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T :=
   match l with
   | CCons x tl =>
     if i = 0#u32
-    then ret x
+    then ok x
     else do
       let i1 ← i - 1#u32
       list_nth T tl i1
@@ -263,7 +263,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
   -- Precondition: the index is in bounds
   (h : ↑i < l.to_list.len)
   -- Postcondition
-  : ∃ x, list_nth T l i = ret x ∧
+  : ∃ x, list_nth T l i = ok x ∧
   -- [x] is the ith element of [l] after conversion to [List]
   x = l.to_list.index ↑i
   := by
@@ -340,7 +340,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
 
    If in a theorem we state and prove that:
    ```
-   ∃ y, i32_id x = ret x
+   ∃ y, i32_id x = ok x
    ```
    we not only prove that the function doesn't fail, but also that it terminates.
 
@@ -348,7 +348,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
    annotates it with the [divergent] keyword.
  -/
 divergent def i32_id (x : I32) : Result I32 :=
-  if x = 0#i32 then ret 0#i32
+  if x = 0#i32 then ok 0#i32
   else do
     let x1 ← x - 1#i32
     let x2 ← i32_id x1
@@ -356,7 +356,7 @@ divergent def i32_id (x : I32) : Result I32 :=
 
 /- We can easily prove that [i32_id] behaves like the identity on positive inputs -/
 theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) :
-  ∃ y, i32_id x = ret y ∧ x.val = y.val := by
+  ∃ y, i32_id x = ok y ∧ x.val = y.val := by
   rw [i32_id]
   if hx : x = 0#i32 then
     simp_all
diff --git a/tests/lean/lake-manifest.json b/tests/lean/lake-manifest.json
index e167e841..404d3dab 100644
--- a/tests/lean/lake-manifest.json
+++ b/tests/lean/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "276953b13323ca151939eafaaec9129bf7970306",
+   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "1c88406514a636d241903e2e288d21dc6d861e01",
+   "rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "6beed82dcfbb7731d173cd517675df27d62ad0f4",
+   "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,16 +31,16 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "af1e86cf7a37389632a02f4a111e6b501b2b818f",
+   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.27",
+   "inputRev": "v0.0.30",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "8079d2d1d0e073bde42eab159c24f4c2d0d3a871",
+   "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "d04f8d39c0e47a0d73450b49f6c0665897cdcaf7",
+   "rev": "d9c412b8103b5098bf8b66cbb981b81a57375925",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -70,5 +70,5 @@
    "inherited": false,
    "dir": "./../../backends/lean",
    "configFile": "lakefile.lean"}],
- "name": "Tests",
+ "name": "tests",
  "lakeDir": ".lake"}
diff --git a/tests/lean/lean-toolchain b/tests/lean/lean-toolchain
index f96d662e..9ad30404 100644
--- a/tests/lean/lean-toolchain
+++ b/tests/lean/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.6.1
+leanprover/lean4:v4.7.0