Merge branch 'son/clean' into checked-ops

13 files changed, 241 insertions, 240 deletions

diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index a57f8bb1..5a85dff0 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -3,7 +3,6 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 -- TODO: there is no Omega tactic for now - it seems it hasn't been ported yet
 --import Mathlib.Tactic.Omega
diff --git a/backends/lean/Base/Diverge.lean b/backends/lean/Base/Diverge.lean
index c9a2eec2..92ffd3cd 100644
--- a/backends/lean/Base/Diverge.lean
+++ b/backends/lean/Base/Diverge.lean
@@ -1,7 +1,6 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 import Base.Diverge.Base
 import Base.Diverge.Elab
diff --git a/backends/lean/Base/Diverge/Base.lean b/backends/lean/Base/Diverge/Base.lean
index e40432bd..0f20125f 100644
--- a/backends/lean/Base/Diverge/Base.lean
+++ b/backends/lean/Base/Diverge/Base.lean
@@ -1,7 +1,6 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 import Base.Primitives.Base
 import Base.Arith.Base
@@ -39,8 +38,7 @@ namespace Lemmas
     case zero =>
       simp_all
       intro m h1 h2
-      have h: n = m := by
-        linarith
+      have h: n = m := by omega
       unfold for_all_fin_aux; simp_all
       simp_all
       -- There is no i s.t. m ≤ i
@@ -169,7 +167,7 @@ namespace Fix
     match x1 with
     | div => True
     | fail _ => x2 = x1
-    | ret _ => x2 = x1 -- TODO: generalize
+    | ok _ => x2 = x1 -- TODO: generalize
 
   -- Monotonicity relation over monadic arrows (i.e., Kleisli arrows)
   def karrow_rel (k1 k2 : (x:a) → Result (b x)) : Prop :=
@@ -388,7 +386,7 @@ namespace Fix
       have Hgeq := Hgmono Hffmono
       simp [result_rel] at Hgeq
       cases Heq: g (fix_fuel n k) <;> rename_i y <;> simp_all
-      -- Remains the .ret case
+      -- Remains the .ok case
       -- Use Hdiv to prove that: ∀ n, h y (fix_fuel n f) = div
       -- We do this in two steps: first we prove it for m ≥ n
       have Hhdiv: ∀ m, h y (fix_fuel m k) = .div := by
@@ -509,7 +507,7 @@ namespace FixI
      specific case.
 
      Remark: the index designates the function in the mutually recursive group
-     (it should be a finite type). We make the return type depend on the input
+     (it should be a finite type). We make the output type depend on the input
      type because we group the type parameters in the input type.
    -/
   open Primitives Fix
@@ -945,7 +943,7 @@ namespace Ex1
     match ls with
     | [] => .fail .panic
     | hd :: tl =>
-      if i = 0 then .ret hd
+      if i = 0 then .ok hd
       else k (tl, i - 1)
 
   theorem list_nth_body_is_valid: ∀ k x, is_valid_p k (λ k => @list_nth_body a k x) := by
@@ -962,7 +960,7 @@ namespace Ex1
       match ls with
       | [] => .fail .panic
       | hd :: tl =>
-        if i = 0 then .ret hd
+        if i = 0 then .ok hd
         else list_nth tl (i - 1)
     := by
     have Heq := is_valid_fix_fixed_eq (@list_nth_body_is_valid a)
@@ -983,11 +981,11 @@ namespace Ex2
     match ls with
     | [] => .fail .panic
     | hd :: tl =>
-      if i = 0 then .ret hd
+      if i = 0 then .ok hd
       else
         do
           let y ← k (tl, i - 1)
-          .ret y
+          .ok y
 
   theorem list_nth_body_is_valid: ∀ k x, is_valid_p k (λ k => @list_nth_body a k x) := by
     intro k x
@@ -1004,11 +1002,11 @@ namespace Ex2
        match ls with
        | [] => .fail .panic
        | hd :: tl =>
-         if i = 0 then .ret hd
+         if i = 0 then .ok hd
          else
            do
              let y ← list_nth tl (i - 1)
-             .ret y)
+             .ok y)
     := by
     have Heq := is_valid_fix_fixed_eq (@list_nth_body_is_valid a)
     simp [list_nth]
@@ -1025,9 +1023,9 @@ namespace Ex3
      - inputs: the sum allows to select the function to call in the recursive
        calls (and the functions may not have the same input types)
      - outputs: this case is degenerate because `even` and `odd` have the same
-       return type `Bool`, but generally speaking we need a sum type because
+       output type `Bool`, but generally speaking we need a sum type because
        the functions in the mutually recursive group may have different
-       return types.
+       output types.
    -/
   variable (k : (Int ⊕ Int) → Result (Bool ⊕ Bool))
 
@@ -1036,7 +1034,7 @@ namespace Ex3
     | .inl i =>
       -- Body of `is_even`
       if i = 0
-      then .ret (.inl true) -- We use .inl because this is `is_even`
+      then .ok (.inl true) -- We use .inl because this is `is_even`
       else
         do
           let b ←
@@ -1046,13 +1044,13 @@ namespace Ex3
               let r ← k (.inr (i- 1))
               match r with
               | .inl _ => .fail .panic -- Invalid output
-              | .inr b => .ret b
-          -- Wrap the return value
-          .ret (.inl b)
+              | .inr b => .ok b
+          -- Wrap the output value
+          .ok (.inl b)
     | .inr i =>
       -- Body of `is_odd`
       if i = 0
-      then .ret (.inr false) -- We use .inr because this is `is_odd`
+      then .ok (.inr false) -- We use .inr because this is `is_odd`
       else
         do
           let b ←
@@ -1061,10 +1059,10 @@ namespace Ex3
               -- extract the output value
               let r ← k (.inl (i- 1))
               match r with
-              | .inl b => .ret b
+              | .inl b => .ok b
               | .inr _ => .fail .panic -- Invalid output
-          -- Wrap the return value
-          .ret (.inr b)
+          -- Wrap the output value
+          .ok (.inr b)
 
   theorem is_even_is_odd_body_is_valid:
     ∀ k x, is_valid_p k (λ k => is_even_is_odd_body k x) := by
@@ -1080,7 +1078,7 @@ namespace Ex3
     do
       let r ← fix is_even_is_odd_body (.inl i)
       match r with
-      | .inl b => .ret b
+      | .inl b => .ok b
       | .inr _ => .fail .panic
 
   def is_odd (i : Int): Result Bool :=
@@ -1088,11 +1086,11 @@ namespace Ex3
       let r ← fix is_even_is_odd_body (.inr i)
       match r with
       | .inl _ => .fail .panic
-      | .inr b => .ret b
+      | .inr b => .ok b
 
   -- The unfolding equation for `is_even` - diverges if `i < 0`
   theorem is_even_eq (i : Int) :
-    is_even i = (if i = 0 then .ret true else is_odd (i - 1))
+    is_even i = (if i = 0 then .ok true else is_odd (i - 1))
     := by
     have Heq := is_valid_fix_fixed_eq is_even_is_odd_body_is_valid
     simp [is_even, is_odd]
@@ -1110,7 +1108,7 @@ namespace Ex3
 
   -- The unfolding equation for `is_odd` - diverges if `i < 0`
   theorem is_odd_eq (i : Int) :
-    is_odd i = (if i = 0 then .ret false else is_even (i - 1))
+    is_odd i = (if i = 0 then .ok false else is_even (i - 1))
     := by
     have Heq := is_valid_fix_fixed_eq is_even_is_odd_body_is_valid
     simp [is_even, is_odd]
@@ -1136,17 +1134,17 @@ namespace Ex4
   /- The bodies are more natural -/
   def is_even_body (k : (i : Fin 2) → (x : input_ty i) → Result (output_ty i x)) (i : Int) : Result Bool :=
     if i = 0
-      then .ret true
+      then .ok true
     else do
       let b ← k 1 (i - 1)
-      .ret b
+      .ok b
 
   def is_odd_body (k : (i : Fin 2) → (x : input_ty i) → Result (output_ty i x)) (i : Int) : Result Bool :=
     if i = 0
-      then .ret false
+      then .ok false
     else do
       let b ← k 0 (i - 1)
-      .ret b
+      .ok b
 
   @[simp] def bodies :
     Funs (Fin 2) input_ty output_ty
@@ -1179,19 +1177,19 @@ namespace Ex4
 
   theorem is_even_eq (i : Int) : is_even i =
     (if i = 0
-       then .ret true
+       then .ok true
      else do
        let b ← is_odd (i - 1)
-       .ret b) := by
+       .ok b) := by
     simp [is_even, is_odd];
     conv => lhs; rw [body_fix_eq]
 
   theorem is_odd_eq (i : Int) : is_odd i =
     (if i = 0
-       then .ret false
+       then .ok false
      else do
        let b ← is_even (i - 1)
-       .ret b) := by
+       .ok b) := by
     simp [is_even, is_odd];
     conv => lhs; rw [body_fix_eq]
 end Ex4
@@ -1205,12 +1203,12 @@ namespace Ex5
   /- An auxiliary function, which doesn't require the fixed-point -/
   def map (f : a → Result b) (ls : List a) : Result (List b) :=
     match ls with
-    | [] => .ret []
+    | [] => .ok []
     | hd :: tl =>
       do
         let hd ← f hd
         let tl ← map f tl
-        .ret (hd :: tl)
+        .ok (hd :: tl)
 
   /- The validity theorem for `map`, generic in `f` -/
   theorem map_is_valid
@@ -1231,11 +1229,11 @@ namespace Ex5
 
   def id_body (k : Tree a → Result (Tree a)) (t : Tree a) : Result (Tree a) :=
     match t with
-    | .leaf x => .ret (.leaf x)
+    | .leaf x => .ok (.leaf x)
     | .node tl =>
       do
         let tl ← map k tl
-        .ret (.node tl)
+        .ok (.node tl)
 
   theorem id_body_is_valid :
     ∀ k x, is_valid_p k (λ k => @id_body a k x) := by
@@ -1256,11 +1254,11 @@ namespace Ex5
   theorem id_eq (t : Tree a) :
     (id t =
        match t with
-       | .leaf x => .ret (.leaf x)
+       | .leaf x => .ok (.leaf x)
        | .node tl =>
        do
          let tl ← map id tl
-         .ret (.node tl))
+         .ok (.node tl))
     := by
     have Heq := is_valid_fix_fixed_eq (@id_body_is_valid a)
     simp [id]
@@ -1285,7 +1283,7 @@ namespace Ex6
     match ls with
     | [] => .fail .panic
     | hd :: tl =>
-      if i = 0 then .ret hd
+      if i = 0 then .ok hd
       else k 0 ⟨ a, tl, i - 1 ⟩
 
   @[simp] def bodies :
@@ -1316,7 +1314,7 @@ namespace Ex6
     match ls with
     | [] => is_valid_p_same k (.fail .panic)
     | hd :: tl =>
-      is_valid_p_ite k (Eq i 0) (is_valid_p_same k (.ret hd)) (is_valid_p_rec k 0 ⟨a, tl, i-1⟩)
+      is_valid_p_ite k (Eq i 0) (is_valid_p_same k (.ok hd)) (is_valid_p_rec k 0 ⟨a, tl, i-1⟩)
 
   theorem body_is_valid' : is_valid body :=
     fun k =>
@@ -1332,7 +1330,7 @@ namespace Ex6
       match ls with
       | [] => .fail .panic
       | hd :: tl =>
-        if i = 0 then .ret hd
+        if i = 0 then .ok hd
         else list_nth tl (i - 1)
     := by
     have Heq := is_valid_fix_fixed_eq body_is_valid
@@ -1347,7 +1345,7 @@ namespace Ex6
       match ls with
       | [] => .fail .panic
       | hd :: tl =>
-        if i = 0 then .ret hd
+        if i = 0 then .ok hd
         else list_nth tl (i - 1)
     :=
     -- Use the fixed-point equation
@@ -1378,7 +1376,7 @@ namespace Ex7
     match ls with
     | [] => .fail .panic
     | hd :: tl =>
-      if i = 0 then .ret hd
+      if i = 0 then .ok hd
       else k 0 a ⟨ tl, i - 1 ⟩
 
   @[simp] def bodies :
@@ -1409,7 +1407,7 @@ namespace Ex7
     match ls with
     | [] => is_valid_p_same k (.fail .panic)
     | hd :: tl =>
-      is_valid_p_ite k (Eq i 0) (is_valid_p_same k (.ret hd)) (is_valid_p_rec k 0 a ⟨tl, i-1⟩)
+      is_valid_p_ite k (Eq i 0) (is_valid_p_same k (.ok hd)) (is_valid_p_rec k 0 a ⟨tl, i-1⟩)
 
   theorem body_is_valid' : is_valid body :=
     fun k =>
@@ -1425,7 +1423,7 @@ namespace Ex7
       match ls with
       | [] => .fail .panic
       | hd :: tl =>
-        if i = 0 then .ret hd
+        if i = 0 then .ok hd
         else list_nth tl (i - 1)
     := by
     have Heq := is_valid_fix_fixed_eq body_is_valid
@@ -1440,7 +1438,7 @@ namespace Ex7
       match ls with
       | [] => .fail .panic
       | hd :: tl =>
-        if i = 0 then .ret hd
+        if i = 0 then .ok hd
         else list_nth tl (i - 1)
     :=
     -- Use the fixed-point equation
@@ -1466,12 +1464,12 @@ namespace Ex8
   /- An auxiliary function, which doesn't require the fixed-point -/
   def map {a : Type y} {b : Type z} (f : a → Result b) (ls : List a) : Result (List b) :=
     match ls with
-    | [] => .ret []
+    | [] => .ok []
     | hd :: tl =>
       do
         let hd ← f hd
         let tl ← map f tl
-        .ret (hd :: tl)
+        .ok (hd :: tl)
 
   /- The validity theorems for `map`, generic in `f` -/
 
@@ -1520,11 +1518,11 @@ namespace Ex9
   def id_body.{u} (k : (i:Fin 1) → (t:ty i) →  input_ty i t → Result (output_ty i t))
     (a : Type u) (t : Tree a) : Result (Tree a) :=
     match t with
-    | .leaf x => .ret (.leaf x)
+    | .leaf x => .ok (.leaf x)
     | .node tl =>
       do
         let tl ← map (k 0 a) tl
-        .ret (.node tl)
+        .ok (.node tl)
 
   @[simp] def bodies :
     Funs (Fin 1) ty input_ty output_ty tys :=
@@ -1558,11 +1556,11 @@ namespace Ex9
   theorem id_eq' {a : Type u} (t : Tree a) :
     id t =
       (match t with
-       | .leaf x => .ret (.leaf x)
+       | .leaf x => .ok (.leaf x)
        | .node tl =>
          do
            let tl ← map id tl
-           .ret (.node tl))
+           .ok (.node tl))
     :=
     -- The unfolding equation
     have Heq := is_valid_fix_fixed_eq body_is_valid.{u}
diff --git a/backends/lean/Base/Diverge/Elab.lean b/backends/lean/Base/Diverge/Elab.lean
index f30148dc..5db8ffed 100644
--- a/backends/lean/Base/Diverge/Elab.lean
+++ b/backends/lean/Base/Diverge/Elab.lean
@@ -1,7 +1,6 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
 import Base.Utils
 import Base.Diverge.Base
 import Base.Diverge.ElabBase
@@ -36,7 +35,7 @@ def mkProd (x y : Expr) : MetaM Expr :=
 def mkInOutTy (x y z : Expr) : MetaM Expr := do
   mkAppM ``FixII.mk_in_out_ty #[x, y, z]
 
--- Return the `a` in `Return a`
+-- Return the `a` in `Result a`
 def getResultTy (ty : Expr) : MetaM Expr :=
   ty.withApp fun f args => do
   if ¬ f.isConstOf ``Result ∨ args.size ≠ 1 then
@@ -412,7 +411,7 @@ structure TypeInfo where
      For `list_nth`: `λ a => List a × Int`
    -/
   in_ty : Expr
-  /- The output type, without the `Return`. This is a function taking
+  /- The output type, without the `Result`. This is a function taking
      as input a value of type `params_ty`.
 
      For `list_nth`: `λ a => a`
@@ -1480,9 +1479,9 @@ namespace Tests
   divergent def list_nth {a: Type u} (ls : List a) (i : Int) : Result a :=
     match ls with
     | [] => .fail .panic
-    | x :: ls =>
-      if i = 0 then return x
-      else return (← list_nth ls (i - 1))
+    | x :: ls => do
+      if i = 0 then pure x
+      else pure (← list_nth ls (i - 1))
 
   --set_option trace.Diverge false
 
@@ -1491,7 +1490,7 @@ namespace Tests
   example {a: Type} (ls : List a) :
     ∀ (i : Int),
     0 ≤ i → i < ls.length →
-    ∃ x, list_nth ls i = .ret x := by
+    ∃ x, list_nth ls i = .ok x := by
     induction ls
     . intro i hpos h; simp at h; linarith
     . rename_i hd tl ih
@@ -1539,7 +1538,7 @@ namespace Tests
       if i > 10 then return (← foo (i / 10)) + (← bar i) else bar 10
 
     divergent def bar (i : Int) : Result Nat :=
-      if i > 20 then foo (i / 20) else .ret 42
+      if i > 20 then foo (i / 20) else .ok 42
   end
 
   #check foo.unfold
@@ -1558,8 +1557,8 @@ namespace Tests
   divergent def iInBounds {a : Type} (ls : List a) (i : Int) : Result Bool :=
     let i0 := ls.length
     if i < i0
-    then Result.ret True
-    else Result.ret False
+    then Result.ok True
+    else Result.ok False
 
   #check iInBounds.unfold
 
@@ -1567,8 +1566,8 @@ namespace Tests
     {a : Type} (ls : List a) : Result Bool :=
     let ls1 := ls
     match ls1 with
-    | [] => Result.ret False
-    | _ :: _ => Result.ret True
+    | [] => Result.ok False
+    | _ :: _ => Result.ok True
 
   #check isCons.unfold
 
@@ -1585,7 +1584,7 @@ namespace Tests
   divergent def infinite_loop : Result Unit :=
     do
     let _ ← infinite_loop
-    Result.ret ()
+    Result.ok ()
 
   #check infinite_loop.unfold
 
@@ -1605,51 +1604,51 @@ namespace Tests
 
     divergent def id {a : Type u} (t : Tree a) : Result (Tree a) :=
       match t with
-      | .leaf x => .ret (.leaf x)
+      | .leaf x => .ok (.leaf x)
       | .node tl =>
         do
           let tl ← map id tl
-          .ret (.node tl)
+          .ok (.node tl)
 
     #check id.unfold
 
     divergent def id1 {a : Type u} (t : Tree a) : Result (Tree a) :=
       match t with
-      | .leaf x => .ret (.leaf x)
+      | .leaf x => .ok (.leaf x)
       | .node tl =>
         do
           let tl ← map (fun x => id1 x) tl
-          .ret (.node tl)
+          .ok (.node tl)
 
     #check id1.unfold
 
     divergent def id2 {a : Type u} (t : Tree a) : Result (Tree a) :=
       match t with
-      | .leaf x => .ret (.leaf x)
+      | .leaf x => .ok (.leaf x)
       | .node tl =>
         do
           let tl ← map (fun x => do let _ ← id2 x; id2 x) tl
-          .ret (.node tl)
+          .ok (.node tl)
 
     #check id2.unfold
 
     divergent def incr (t : Tree Nat) : Result (Tree Nat) :=
       match t with
-      | .leaf x => .ret (.leaf (x + 1))
+      | .leaf x => .ok (.leaf (x + 1))
       | .node tl =>
         do
           let tl ← map incr tl
-          .ret (.node tl)
+          .ok (.node tl)
 
     -- We handle this by inlining the let-binding
     divergent def id3 (t : Tree Nat) : Result (Tree Nat) :=
       match t with
-      | .leaf x => .ret (.leaf (x + 1))
+      | .leaf x => .ok (.leaf (x + 1))
       | .node tl =>
         do
           let f := id3
           let tl ← map f tl
-          .ret (.node tl)
+          .ok (.node tl)
 
     #check id3.unfold
 
@@ -1659,12 +1658,12 @@ namespace Tests
     -- be parameterized by something).
     divergent def id4 (t : Tree Nat) : Result (Tree Nat) :=
       match t with
-      | .leaf x => .ret (.leaf (x + 1))
+      | .leaf x => .ok (.leaf (x + 1))
       | .node tl =>
         do
-          let f ← .ret id4
+          let f ← .ok id4
           let tl ← map f tl
-          .ret (.node tl)
+          .ok (.node tl)
 
     #check id4.unfold
     -/
diff --git a/backends/lean/Base/Primitives/Alloc.lean b/backends/lean/Base/Primitives/Alloc.lean
index 1f470fe1..15fe1ff9 100644
--- a/backends/lean/Base/Primitives/Alloc.lean
+++ b/backends/lean/Base/Primitives/Alloc.lean
@@ -11,8 +11,8 @@ namespace boxed -- alloc.boxed
 
 namespace Box -- alloc.boxed.Box
 
-def deref (T : Type) (x : T) : Result T := ret x
-def deref_mut (T : Type) (x : T) : Result (T × (T → Result T)) := ret (x, λ x => ret x)
+def deref (T : Type) (x : T) : Result T := ok x
+def deref_mut (T : Type) (x : T) : Result (T × (T → Result T)) := ok (x, λ x => ok x)
 
 /-- Trait instance -/
 def coreopsDerefInst (Self : Type) :
diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index e1a39d40..91ca7284 100644
--- a/backends/lean/Base/Primitives/ArraySlice.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -2,7 +2,6 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 import Base.IList
 import Base.Primitives.Scalar
@@ -50,7 +49,7 @@ abbrev Array.slice {α : Type u} {n : Usize} [Inhabited α] (v : Array α n) (i
 def Array.index_usize (α : Type u) (n : Usize) (v: Array α n) (i: Usize) : Result α :=
   match v.val.indexOpt i.val with
   | none => fail .arrayOutOfBounds
-  | some x => ret x
+  | some x => ok x
 
 -- For initialization
 def Array.repeat (α : Type u) (n : Usize) (x : α) : Array α n :=
@@ -69,7 +68,7 @@ theorem Array.repeat_spec {α : Type u} (n : Usize) (x : α) :
 @[pspec]
 theorem Array.index_usize_spec {α : Type u} {n : Usize} [Inhabited α] (v: Array α n) (i: Usize)
   (hbound : i.val < v.length) :
-  ∃ x, v.index_usize α n i = ret x ∧ x = v.val.index i.val := by
+  ∃ x, v.index_usize α n i = ok x ∧ x = v.val.index i.val := by
   simp only [index_usize]
   -- TODO: dependent rewrite
   have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
@@ -79,12 +78,12 @@ def Array.update_usize (α : Type u) (n : Usize) (v: Array α n) (i: Usize) (x:
   match v.val.indexOpt i.val with
   | none => fail .arrayOutOfBounds
   | some _ =>
-    .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
+    ok ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
 
 @[pspec]
 theorem Array.update_usize_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize) (x : α)
   (hbound : i.val < v.length) :
-  ∃ nv, v.update_usize α n i x = ret nv ∧
+  ∃ nv, v.update_usize α n i x = ok nv ∧
   nv.val = v.val.update i.val x
   := by
   simp only [update_usize]
@@ -96,12 +95,12 @@ theorem Array.update_usize_spec {α : Type u} {n : Usize} (v: Array α n) (i: Us
 def Array.index_mut_usize (α : Type u) (n : Usize) (v: Array α n) (i: Usize) :
   Result (α × (α -> Result (Array α n))) := do
   let x ← index_usize α n v i
-  ret (x, update_usize α n v i)
+  ok (x, update_usize α n v i)
 
 @[pspec]
 theorem Array.index_mut_usize_spec {α : Type u} {n : Usize} [Inhabited α] (v: Array α n) (i: Usize)
   (hbound : i.val < v.length) :
-  ∃ x back, v.index_mut_usize α n i = ret (x, back) ∧
+  ∃ x back, v.index_mut_usize α n i = ok (x, back) ∧
   x = v.val.index i.val ∧
   back = update_usize α n v i := by
   simp only [index_mut_usize, Bind.bind, bind]
@@ -148,7 +147,7 @@ abbrev Slice.slice {α : Type u} [Inhabited α] (s : Slice α) (i j : Int) : Lis
 def Slice.index_usize (α : Type u) (v: Slice α) (i: Usize) : Result α :=
   match v.val.indexOpt i.val with
   | none => fail .arrayOutOfBounds
-  | some x => ret x
+  | some x => ok x
 
 /- In the theorems below: we don't always need the `∃ ..`, but we use one
    so that `progress` introduces an opaque variable and an equality. This
@@ -158,7 +157,7 @@ def Slice.index_usize (α : Type u) (v: Slice α) (i: Usize) : Result α :=
 @[pspec]
 theorem Slice.index_usize_spec {α : Type u} [Inhabited α] (v: Slice α) (i: Usize)
   (hbound : i.val < v.length) :
-  ∃ x, v.index_usize α i = ret x ∧ x = v.val.index i.val := by
+  ∃ x, v.index_usize α i = ok x ∧ x = v.val.index i.val := by
   simp only [index_usize]
   -- TODO: dependent rewrite
   have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
@@ -168,12 +167,12 @@ def Slice.update_usize (α : Type u) (v: Slice α) (i: Usize) (x: α) : Result (
   match v.val.indexOpt i.val with
   | none => fail .arrayOutOfBounds
   | some _ =>
-    .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
+    ok ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
 
 @[pspec]
 theorem Slice.update_usize_spec {α : Type u} (v: Slice α) (i: Usize) (x : α)
   (hbound : i.val < v.length) :
-  ∃ nv, v.update_usize α i x = ret nv ∧
+  ∃ nv, v.update_usize α i x = ok nv ∧
   nv.val = v.val.update i.val x
   := by
   simp only [update_usize]
@@ -185,12 +184,12 @@ theorem Slice.update_usize_spec {α : Type u} (v: Slice α) (i: Usize) (x : α)
 def Slice.index_mut_usize (α : Type u) (v: Slice α) (i: Usize) :
   Result (α × (α → Result (Slice α))) := do
   let x ← Slice.index_usize α v i
-  ret (x, Slice.update_usize α v i)
+  ok (x, Slice.update_usize α v i)
 
 @[pspec]
 theorem Slice.index_mut_usize_spec {α : Type u} [Inhabited α] (v: Slice α) (i: Usize)
   (hbound : i.val < v.length) :
-  ∃ x back, v.index_mut_usize α i = ret (x, back) ∧
+  ∃ x back, v.index_mut_usize α i = ok (x, back) ∧
   x = v.val.index i.val ∧
   back = Slice.update_usize α v i := by
   simp only [index_mut_usize, Bind.bind, bind]
@@ -204,30 +203,30 @@ theorem Slice.index_mut_usize_spec {α : Type u} [Inhabited α] (v: Slice α) (i
    `progress` tactic), meaning `Array.to_slice` should be considered as opaque.
    All what the spec theorem reveals is that the "representative" lists are the same. -/
 def Array.to_slice (α : Type u) (n : Usize) (v : Array α n) : Result (Slice α) :=
-  ret ⟨ v.val, by simp [← List.len_eq_length]; scalar_tac ⟩
+  ok ⟨ v.val, by simp [← List.len_eq_length]; scalar_tac ⟩
 
 @[pspec]
 theorem Array.to_slice_spec {α : Type u} {n : Usize} (v : Array α n) :
-  ∃ s, to_slice α n v = ret s ∧ v.val = s.val := by simp [to_slice]
+  ∃ s, to_slice α n v = ok s ∧ v.val = s.val := by simp [to_slice]
 
 def Array.from_slice (α : Type u) (n : Usize) (_ : Array α n) (s : Slice α) : Result (Array α n) :=
   if h: s.val.len = n.val then
-    ret ⟨ s.val, by simp [← List.len_eq_length, *] ⟩
+    ok ⟨ s.val, by simp [← List.len_eq_length, *] ⟩
   else fail panic
 
 @[pspec]
 theorem Array.from_slice_spec {α : Type u} {n : Usize} (a : Array α n) (ns : Slice α) (h : ns.val.len = n.val) :
-  ∃ na, from_slice α n a ns = ret na ∧ na.val = ns.val
+  ∃ na, from_slice α n a ns = ok na ∧ na.val = ns.val
   := by simp [from_slice, *]
 
 def Array.to_slice_mut (α : Type u) (n : Usize) (a : Array α n) :
   Result (Slice α × (Slice α → Result (Array α n))) := do
   let s ← Array.to_slice α n a
-  ret (s, Array.from_slice α n a)
+  ok (s, Array.from_slice α n a)
 
 @[pspec]
 theorem Array.to_slice_mut_spec {α : Type u} {n : Usize} (v : Array α n) :
-  ∃ s back, to_slice_mut α n v = ret (s, back) ∧
+  ∃ s back, to_slice_mut α n v = ok (s, back) ∧
   v.val = s.val ∧
   back = Array.from_slice α n v
   := by simp [to_slice_mut, to_slice]
@@ -235,7 +234,7 @@ theorem Array.to_slice_mut_spec {α : Type u} {n : Usize} (v : Array α n) :
 def Array.subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) : Result (Slice α) :=
   -- TODO: not completely sure here
   if r.start.val < r.end_.val ∧ r.end_.val ≤ a.val.len then
-    ret ⟨ a.val.slice r.start.val r.end_.val,
+    ok ⟨ a.val.slice r.start.val r.end_.val,
           by
             simp [← List.len_eq_length]
             have := a.val.slice_len_le r.start.val r.end_.val
@@ -246,7 +245,7 @@ def Array.subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize)
 @[pspec]
 theorem Array.subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize)
   (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ a.val.len) :
-  ∃ s, subslice α n a r = ret s ∧
+  ∃ s, subslice α n a r = ok s ∧
   s.val = a.val.slice r.start.val r.end_.val ∧
   (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → s.val.index i = a.val.index (r.start.val + i))
   := by
@@ -269,8 +268,8 @@ def Array.update_subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range
       . scalar_tac
       . scalar_tac
     let na := s_beg.append (s.val.append s_end)
-    have : na.len = a.val.len := by simp [*]
-    ret ⟨ na, by simp_all [← List.len_eq_length]; scalar_tac ⟩
+    have : na.len = a.val.len := by simp [na, *]
+    ok ⟨ na, by simp_all [← List.len_eq_length]; scalar_tac ⟩
   else
     fail panic
 
@@ -282,7 +281,7 @@ def Array.update_subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range
 @[pspec]
 theorem Array.update_subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize) (s : Slice α)
   (_ : r.start.val < r.end_.val) (_ : r.end_.val ≤ a.length) (_ : s.length = r.end_.val - r.start.val) :
-  ∃ na, update_subslice α n a r s = ret na ∧
+  ∃ na, update_subslice α n a r s = ok na ∧
   (∀ i, 0 ≤ i → i < r.start.val → na.index_s i = a.index_s i) ∧
   (∀ i, r.start.val ≤ i → i < r.end_.val → na.index_s i = s.index_s (i - r.start.val)) ∧
   (∀ i, r.end_.val ≤ i → i < n.val → na.index_s i = a.index_s i) := by
@@ -306,7 +305,7 @@ theorem Array.update_subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a :
 def Slice.subslice (α : Type u) (s : Slice α) (r : Range Usize) : Result (Slice α) :=
   -- TODO: not completely sure here
   if r.start.val < r.end_.val ∧ r.end_.val ≤ s.length then
-    ret ⟨ s.val.slice r.start.val r.end_.val,
+    ok ⟨ s.val.slice r.start.val r.end_.val,
           by
             simp [← List.len_eq_length]
             have := s.val.slice_len_le r.start.val r.end_.val
@@ -317,7 +316,7 @@ def Slice.subslice (α : Type u) (s : Slice α) (r : Range Usize) : Result (Slic
 @[pspec]
 theorem Slice.subslice_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Range Usize)
   (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ s.val.len) :
-  ∃ ns, subslice α s r = ret ns ∧
+  ∃ ns, subslice α s r = ok ns ∧
   ns.val = s.slice r.start.val r.end_.val ∧
   (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → ns.index_s i = s.index_s (r.start.val + i))
   := by
@@ -343,15 +342,15 @@ def Slice.update_subslice (α : Type u) (s : Slice α) (r : Range Usize) (ss : S
       . scalar_tac
       . scalar_tac
     let ns := s_beg.append (ss.val.append s_end)
-    have : ns.len = s.val.len := by simp [*]
-    ret ⟨ ns, by simp_all [← List.len_eq_length]; scalar_tac ⟩
+    have : ns.len = s.val.len := by simp [ns, *]
+    ok ⟨ ns, by simp_all [← List.len_eq_length]; scalar_tac ⟩
   else
     fail panic
 
 @[pspec]
 theorem Slice.update_subslice_spec {α : Type u} [Inhabited α] (a : Slice α) (r : Range Usize) (ss : Slice α)
   (_ : r.start.val < r.end_.val) (_ : r.end_.val ≤ a.length) (_ : ss.length = r.end_.val - r.start.val) :
-  ∃ na, update_subslice α a r ss = ret na ∧
+  ∃ na, update_subslice α a r ss = ok na ∧
   (∀ i, 0 ≤ i → i < r.start.val → na.index_s i = a.index_s i) ∧
   (∀ i, r.start.val ≤ i → i < r.end_.val → na.index_s i = ss.index_s (i - r.start.val)) ∧
   (∀ i, r.end_.val ≤ i → i < a.length → na.index_s i = a.index_s i) := by
@@ -393,7 +392,7 @@ def core.slice.index.Slice.index
   let x ← inst.get i slice
   match x with
   | none => fail panic
-  | some x => ret x
+  | some x => ok x
 
 /- [core::slice::index::Range:::get]: forward function -/
 def core.slice.index.RangeUsize.get (T : Type) (i : Range Usize) (slice : Slice T) :
diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean
index 0c64eca1..4c5b2795 100644
--- a/backends/lean/Base/Primitives/Base.lean
+++ b/backends/lean/Base/Primitives/Base.lean
@@ -41,7 +41,7 @@ deriving Repr, BEq
 open Error
 
 inductive Result (α : Type u) where
-  | ret (v: α): Result α
+  | ok (v: α): Result α
   | fail (e: Error): Result α
   | div
 deriving Repr, BEq
@@ -56,31 +56,31 @@ instance Result_Nonempty (α : Type u) : Nonempty (Result α) :=
 
 /- HELPERS -/
 
-def ret? {α: Type u} (r: Result α): Bool :=
+def ok? {α: Type u} (r: Result α): Bool :=
   match r with
-  | ret _ => true
+  | ok _ => true
   | fail _ | div => false
 
 def div? {α: Type u} (r: Result α): Bool :=
   match r with
   | div => true
-  | ret _ | fail _ => false
+  | ok _ | fail _ => false
 
 def massert (b:Bool) : Result Unit :=
-  if b then ret () else fail assertionFailure
+  if b then ok () else fail assertionFailure
 
 macro "prove_eval_global" : tactic => `(tactic| first | apply Eq.refl | decide)
 
-def eval_global {α: Type u} (x: Result α) (_: ret? x := by prove_eval_global) : α :=
+def eval_global {α: Type u} (x: Result α) (_: ok? x := by prove_eval_global) : α :=
   match x with
   | fail _ | div => by contradiction
-  | ret x => x
+  | ok x => x
 
 /- DO-DSL SUPPORT -/
 
 def bind {α : Type u} {β : Type v} (x: Result α) (f: α → Result β) : Result β :=
   match x with
-  | ret v  => f v
+  | ok v  => f v
   | fail v => fail v
   | div => div
 
@@ -88,11 +88,11 @@ def bind {α : Type u} {β : Type v} (x: Result α) (f: α → Result β) : Resu
 instance : Bind Result where
   bind := bind
 
--- Allows using return x in do-blocks
+-- Allows using pure x in do-blocks
 instance : Pure Result where
-  pure := fun x => ret x
+  pure := fun x => ok x
 
-@[simp] theorem bind_ret (x : α) (f : α → Result β) : bind (.ret x) f = f x := by simp [bind]
+@[simp] theorem bind_ok (x : α) (f : α → Result β) : bind (.ok x) f = f x := by simp [bind]
 @[simp] theorem bind_fail (x : Error) (f : α → Result β) : bind (.fail x) f = .fail x := by simp [bind]
 @[simp] theorem bind_div (f : α → Result β) : bind .div f = .div := by simp [bind]
 
@@ -103,14 +103,14 @@ instance : Pure Result where
 -- rely on subtype, and a custom let-binding operator, in effect recreating our
 -- own variant of the do-dsl
 
-def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } :=
+def Result.attach {α: Type} (o : Result α): Result { x : α // o = ok x } :=
   match o with
-  | ret x => ret ⟨x, rfl⟩
+  | ok x => ok ⟨x, rfl⟩
   | fail e => fail e
   | div => div
 
-@[simp] theorem bind_tc_ret (x : α) (f : α → Result β) :
-  (do let y ← .ret x; f y) = f x := by simp [Bind.bind, bind]
+@[simp] theorem bind_tc_ok (x : α) (f : α → Result β) :
+  (do let y ← .ok x; f y) = f x := by simp [Bind.bind, bind]
 
 @[simp] theorem bind_tc_fail (x : Error) (f : α → Result β) :
   (do let y ← fail x; f y) = fail x := by simp [Bind.bind, bind]
diff --git a/backends/lean/Base/Primitives/Range.lean b/backends/lean/Base/Primitives/Range.lean
index a268bcba..416cd201 100644
--- a/backends/lean/Base/Primitives/Range.lean
+++ b/backends/lean/Base/Primitives/Range.lean
@@ -2,7 +2,6 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 import Base.IList
 import Base.Primitives.Scalar
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index f46aded9..53bc7854 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -265,6 +265,14 @@ theorem Scalar.cMax_suffices ty (h : x ≤ Scalar.cMax ty) : x ≤ Scalar.max ty
   have := Scalar.cMax_bound ty
   linarith
 
+/-- The scalar type.
+
+    We could use a subtype, but it using a custom structure type allows us
+    to have more control over the coercions and the simplifications (we tried
+    using a subtype and it caused issues especially as we had to make the Scalar
+    type non-reducible, so that we could have more control, but leading to
+    some natural equalities not being obvious to the simplifier anymore).
+ -/
 structure Scalar (ty : ScalarTy) where
   val : Int
   hmin : Scalar.min ty ≤ val
@@ -274,6 +282,9 @@ deriving Repr
 instance (ty : ScalarTy) : CoeOut (Scalar ty) Int where
   coe := λ v => v.val
 
+/- Activate the ↑ notation -/
+attribute [coe] Scalar.val
+
 theorem Scalar.bound_suffices (ty : ScalarTy) (x : Int) :
   Scalar.cMin ty ≤ x ∧ x ≤ Scalar.cMax ty ->
   Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty
@@ -339,7 +350,7 @@ def Scalar.tryMk (ty : ScalarTy) (x : Int) : Result (Scalar ty) :=
     -- ```
     -- then normalization blocks (for instance, some proofs which use reflexivity fail).
     -- However, the version below doesn't block reduction (TODO: investigate):
-    return Scalar.ofIntCore x (Scalar.check_bounds_prop h)
+    ok (Scalar.ofIntCore x (Scalar.check_bounds_prop h))
   else fail integerOverflow
 
 def Scalar.neg {ty : ScalarTy} (x : Scalar ty) : Result (Scalar ty) := Scalar.tryMk ty (- x.val)
@@ -602,7 +613,7 @@ def core.num.checked_mod (x y : Scalar ty) : Result (Option (Scalar ty)) :=
 theorem Scalar.add_spec {ty} {x y : Scalar ty}
   (hmin : Scalar.min ty ≤ ↑x + y.val)
   (hmax : ↑x + ↑y ≤ Scalar.max ty) :
-  (∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y) := by
+  (∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y) := by
   -- Applying the unfoldings only on the left
   conv => congr; ext; lhs; unfold HAdd.hAdd instHAddScalarResult; simp [add, tryMk]
   split
@@ -611,7 +622,7 @@ theorem Scalar.add_spec {ty} {x y : Scalar ty}
 
 theorem Scalar.add_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
   (hmax : ↑x + ↑y ≤ Scalar.max ty) :
-  ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
+  ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by
   have hmin : Scalar.min ty ≤ ↑x + ↑y := by
     have hx := x.hmin
     have hy := y.hmin
@@ -620,57 +631,57 @@ theorem Scalar.add_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
 
 /- Fine-grained theorems -/
 @[pspec] theorem Usize.add_spec {x y : Usize} (hmax : ↑x + ↑y ≤ Usize.max) :
-  ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
+  ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by
   apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
 
 @[pspec] theorem U8.add_spec {x y : U8} (hmax : ↑x + ↑y ≤ U8.max) :
-  ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
+  ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by
   apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
 
 @[pspec] theorem U16.add_spec {x y : U16} (hmax : ↑x + ↑y ≤ U16.max) :
-  ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
+  ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by
   apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
 
 @[pspec] theorem U32.add_spec {x y : U32} (hmax : ↑x + ↑y ≤ U32.max) :
-  ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
+  ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by
   apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
 
 @[pspec] theorem U64.add_spec {x y : U64} (hmax : ↑x + ↑y ≤ U64.max) :
-  ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
+  ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by
   apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
 
 @[pspec] theorem U128.add_spec {x y : U128} (hmax : ↑x + ↑y ≤ U128.max) :
-  ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y := by
+  ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by
   apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
 
 @[pspec] theorem Isize.add_spec {x y : Isize}
   (hmin : Isize.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ Isize.max) :
-  ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y :=
+  ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y :=
   Scalar.add_spec hmin hmax
 
 @[pspec] theorem I8.add_spec {x y : I8}
   (hmin : I8.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ I8.max) :
-  ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y :=
+  ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y :=
   Scalar.add_spec hmin hmax
 
 @[pspec] theorem I16.add_spec {x y : I16}
   (hmin : I16.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ I16.max) :
-  ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y :=
+  ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y :=
   Scalar.add_spec hmin hmax
 
 @[pspec] theorem I32.add_spec {x y : I32}
   (hmin : I32.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ I32.max) :
-  ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y :=
+  ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y :=
   Scalar.add_spec hmin hmax
 
 @[pspec] theorem I64.add_spec {x y : I64}
   (hmin : I64.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ I64.max) :
-  ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y :=
+  ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y :=
   Scalar.add_spec hmin hmax
 
 @[pspec] theorem I128.add_spec {x y : I128}
   (hmin : I128.min ≤ ↑x + ↑y) (hmax : ↑x + ↑y ≤ I128.max) :
-  ∃ z, x + y = ret z ∧ (↑z : Int) = ↑x + ↑y :=
+  ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y :=
   Scalar.add_spec hmin hmax
 
 -- Generic theorem - shouldn't be used much
@@ -678,7 +689,7 @@ theorem Scalar.add_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
 theorem Scalar.sub_spec {ty} {x y : Scalar ty}
   (hmin : Scalar.min ty ≤ ↑x - ↑y)
   (hmax : ↑x - ↑y ≤ Scalar.max ty) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
   conv => congr; ext; lhs; simp [HSub.hSub, sub, tryMk, Sub.sub]
   split
   . simp [pure]
@@ -687,7 +698,7 @@ theorem Scalar.sub_spec {ty} {x y : Scalar ty}
 
 theorem Scalar.sub_unsigned_spec {ty : ScalarTy} (s : ¬ ty.isSigned)
   {x y : Scalar ty} (hmin : Scalar.min ty ≤ ↑x - ↑y) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
   have : ↑x - ↑y ≤ Scalar.max ty := by
     have hx := x.hmin
     have hxm := x.hmax
@@ -698,64 +709,64 @@ theorem Scalar.sub_unsigned_spec {ty : ScalarTy} (s : ¬ ty.isSigned)
 
 /- Fine-grained theorems -/
 @[pspec] theorem Usize.sub_spec {x y : Usize} (hmin : Usize.min ≤ ↑x - ↑y) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
   apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
 
 @[pspec] theorem U8.sub_spec {x y : U8} (hmin : U8.min ≤ ↑x - ↑y) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
   apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
 
 @[pspec] theorem U16.sub_spec {x y : U16} (hmin : U16.min ≤ ↑x - ↑y) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
   apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
 
 @[pspec] theorem U32.sub_spec {x y : U32} (hmin : U32.min ≤ ↑x - ↑y) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
   apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
 
 @[pspec] theorem U64.sub_spec {x y : U64} (hmin : U64.min ≤ ↑x - ↑y) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
   apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
 
 @[pspec] theorem U128.sub_spec {x y : U128} (hmin : U128.min ≤ ↑x - ↑y) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y := by
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
   apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
 
 @[pspec] theorem Isize.sub_spec {x y : Isize} (hmin : Isize.min ≤ ↑x - ↑y)
   (hmax : ↑x - ↑y ≤ Isize.max) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y :=
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y :=
   Scalar.sub_spec hmin hmax
 
 @[pspec] theorem I8.sub_spec {x y : I8} (hmin : I8.min ≤ ↑x - ↑y)
   (hmax : ↑x - ↑y ≤ I8.max) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y :=
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y :=
   Scalar.sub_spec hmin hmax
 
 @[pspec] theorem I16.sub_spec {x y : I16} (hmin : I16.min ≤ ↑x - ↑y)
   (hmax : ↑x - ↑y ≤ I16.max) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y :=
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y :=
   Scalar.sub_spec hmin hmax
 
 @[pspec] theorem I32.sub_spec {x y : I32} (hmin : I32.min ≤ ↑x - ↑y)
   (hmax : ↑x - ↑y ≤ I32.max) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y :=
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y :=
   Scalar.sub_spec hmin hmax
 
 @[pspec] theorem I64.sub_spec {x y : I64} (hmin : I64.min ≤ ↑x - ↑y)
   (hmax : ↑x - ↑y ≤ I64.max) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y :=
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y :=
   Scalar.sub_spec hmin hmax
 
 @[pspec] theorem I128.sub_spec {x y : I128} (hmin : I128.min ≤ ↑x - ↑y)
   (hmax : ↑x - ↑y ≤ I128.max) :
-  ∃ z, x - y = ret z ∧ (↑z : Int) = ↑x - ↑y :=
+  ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y :=
   Scalar.sub_spec hmin hmax
 
 -- Generic theorem - shouldn't be used much
 theorem Scalar.mul_spec {ty} {x y : Scalar ty}
   (hmin : Scalar.min ty ≤ ↑x * ↑y)
   (hmax : ↑x * ↑y ≤ Scalar.max ty) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
   conv => congr; ext; lhs; simp [HMul.hMul]
   simp [mul, tryMk]
   split
@@ -765,7 +776,7 @@ theorem Scalar.mul_spec {ty} {x y : Scalar ty}
 
 theorem Scalar.mul_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
   (hmax : ↑x * ↑y ≤ Scalar.max ty) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
   have : Scalar.min ty ≤ ↑x * ↑y := by
     have hx := x.hmin
     have hy := y.hmin
@@ -774,57 +785,57 @@ theorem Scalar.mul_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
 
 /- Fine-grained theorems -/
 @[pspec] theorem Usize.mul_spec {x y : Usize} (hmax : ↑x * ↑y ≤ Usize.max) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
   apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
 
 @[pspec] theorem U8.mul_spec {x y : U8} (hmax : ↑x * ↑y ≤ U8.max) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
   apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
 
 @[pspec] theorem U16.mul_spec {x y : U16} (hmax : ↑x * ↑y ≤ U16.max) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
   apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
 
 @[pspec] theorem U32.mul_spec {x y : U32} (hmax : ↑x * ↑y ≤ U32.max) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
   apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
 
 @[pspec] theorem U64.mul_spec {x y : U64} (hmax : ↑x * ↑y ≤ U64.max) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
   apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
 
 @[pspec] theorem U128.mul_spec {x y : U128} (hmax : ↑x * ↑y ≤ U128.max) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y := by
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
   apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
 
 @[pspec] theorem Isize.mul_spec {x y : Isize} (hmin : Isize.min ≤ ↑x * ↑y)
   (hmax : ↑x * ↑y ≤ Isize.max) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y :=
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y :=
   Scalar.mul_spec hmin hmax
 
 @[pspec] theorem I8.mul_spec {x y : I8} (hmin : I8.min ≤ ↑x * ↑y)
   (hmax : ↑x * ↑y ≤ I8.max) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y :=
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y :=
   Scalar.mul_spec hmin hmax
 
 @[pspec] theorem I16.mul_spec {x y : I16} (hmin : I16.min ≤ ↑x * ↑y)
   (hmax : ↑x * ↑y ≤ I16.max) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y :=
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y :=
   Scalar.mul_spec hmin hmax
 
 @[pspec] theorem I32.mul_spec {x y : I32} (hmin : I32.min ≤ ↑x * ↑y)
   (hmax : ↑x * ↑y ≤ I32.max) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y :=
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y :=
   Scalar.mul_spec hmin hmax
 
 @[pspec] theorem I64.mul_spec {x y : I64} (hmin : I64.min ≤ ↑x * ↑y)
   (hmax : ↑x * ↑y ≤ I64.max) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y :=
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y :=
   Scalar.mul_spec hmin hmax
 
 @[pspec] theorem I128.mul_spec {x y : I128} (hmin : I128.min ≤ ↑x * ↑y)
   (hmax : ↑x * ↑y ≤ I128.max) :
-  ∃ z, x * y = ret z ∧ (↑z : Int) = ↑x * ↑y :=
+  ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y :=
   Scalar.mul_spec hmin hmax
 
 -- Generic theorem - shouldn't be used much
@@ -833,15 +844,14 @@ theorem Scalar.div_spec {ty} {x y : Scalar ty}
   (hnz : ↑y ≠ (0 : Int))
   (hmin : Scalar.min ty ≤ scalar_div ↑x ↑y)
   (hmax : scalar_div ↑x ↑y ≤ Scalar.max ty) :
-  ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y := by
+  ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y := by
   simp [HDiv.hDiv, div, Div.div]
   simp [tryMk, *]
-  simp [pure]
   rfl
 
 theorem Scalar.div_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : Scalar ty}
   (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
+  ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by
   have h : Scalar.min ty = 0 := by cases ty <;> simp [ScalarTy.isSigned, min] at *
   have hx := x.hmin
   have hy := y.hmin
@@ -857,69 +867,69 @@ theorem Scalar.div_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S
 
 /- Fine-grained theorems -/
 @[pspec] theorem Usize.div_spec (x : Usize) {y : Usize} (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
+  ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by
   apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *]
 
 @[pspec] theorem U8.div_spec (x : U8) {y : U8} (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
+  ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by
   apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *]
 
 @[pspec] theorem U16.div_spec (x : U16) {y : U16} (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
+  ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by
   apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *]
 
 @[pspec] theorem U32.div_spec (x : U32) {y : U32} (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
+  ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by
   apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *]
 
 @[pspec] theorem U64.div_spec (x : U64) {y : U64} (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
+  ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by
   apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *]
 
 @[pspec] theorem U128.div_spec (x : U128) {y : U128} (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x / y = ret z ∧ (↑z : Int) = ↑x / ↑y := by
+  ∃ z, x / y = ok z ∧ (↑z : Int) = ↑x / ↑y := by
   apply Scalar.div_unsigned_spec <;> simp [ScalarTy.isSigned, *]
 
 @[pspec] theorem Isize.div_spec (x : Isize) {y : Isize}
   (hnz : ↑y ≠ (0 : Int))
   (hmin : Isize.min ≤ scalar_div ↑x ↑y)
   (hmax : scalar_div ↑x ↑y ≤ Isize.max):
-  ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
+  ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
   Scalar.div_spec hnz hmin hmax
 
 @[pspec] theorem I8.div_spec (x : I8) {y : I8}
   (hnz : ↑y ≠ (0 : Int))
   (hmin : I8.min ≤ scalar_div ↑x ↑y)
   (hmax : scalar_div ↑x ↑y ≤ I8.max):
-  ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
+  ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
   Scalar.div_spec hnz hmin hmax
 
 @[pspec] theorem I16.div_spec (x : I16) {y : I16}
   (hnz : ↑y ≠ (0 : Int))
   (hmin : I16.min ≤ scalar_div ↑x ↑y)
   (hmax : scalar_div ↑x ↑y ≤ I16.max):
-  ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
+  ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
   Scalar.div_spec hnz hmin hmax
 
 @[pspec] theorem I32.div_spec (x : I32) {y : I32}
   (hnz : ↑y ≠ (0 : Int))
   (hmin : I32.min ≤ scalar_div ↑x ↑y)
   (hmax : scalar_div ↑x ↑y ≤ I32.max):
-  ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
+  ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
   Scalar.div_spec hnz hmin hmax
 
 @[pspec] theorem I64.div_spec (x : I64) {y : I64}
   (hnz : ↑y ≠ (0 : Int))
   (hmin : I64.min ≤ scalar_div ↑x ↑y)
   (hmax : scalar_div ↑x ↑y ≤ I64.max):
-  ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
+  ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
   Scalar.div_spec hnz hmin hmax
 
 @[pspec] theorem I128.div_spec (x : I128) {y : I128}
   (hnz : ↑y ≠ (0 : Int))
   (hmin : I128.min ≤ scalar_div ↑x ↑y)
   (hmax : scalar_div ↑x ↑y ≤ I128.max):
-  ∃ z, x / y = ret z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
+  ∃ z, x / y = ok z ∧ (↑z : Int) = scalar_div ↑x ↑y :=
   Scalar.div_spec hnz hmin hmax
 
 -- Generic theorem - shouldn't be used much
@@ -928,15 +938,14 @@ theorem Scalar.rem_spec {ty} {x y : Scalar ty}
   (hnz : ↑y ≠ (0 : Int))
   (hmin : Scalar.min ty ≤ scalar_rem ↑x ↑y)
   (hmax : scalar_rem ↑x ↑y ≤ Scalar.max ty) :
-  ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y := by
+  ∃ z, x % y = ok z ∧ (↑z : Int) = scalar_rem ↑x ↑y := by
   simp [HMod.hMod, rem]
   simp [tryMk, *]
-  simp [pure]
   rfl
 
 theorem Scalar.rem_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : Scalar ty}
   (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
+  ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by
   have h : Scalar.min ty = 0 := by cases ty <;> simp [ScalarTy.isSigned, min] at *
   have hx := x.hmin
   have hy := y.hmin
@@ -952,62 +961,62 @@ theorem Scalar.rem_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S
   simp [*]
 
 @[pspec] theorem Usize.rem_spec (x : Usize) {y : Usize} (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
+  ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by
   apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *]
 
 @[pspec] theorem U8.rem_spec (x : U8) {y : U8} (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
+  ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by
   apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *]
 
 @[pspec] theorem U16.rem_spec (x : U16) {y : U16} (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
+  ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by
   apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *]
 
 @[pspec] theorem U32.rem_spec (x : U32) {y : U32} (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
+  ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by
   apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *]
 
 @[pspec] theorem U64.rem_spec (x : U64) {y : U64} (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
+  ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by
   apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *]
 
 @[pspec] theorem U128.rem_spec (x : U128) {y : U128} (hnz : ↑y ≠ (0 : Int)) :
-  ∃ z, x % y = ret z ∧ (↑z : Int) = ↑x % ↑y := by
+  ∃ z, x % y = ok z ∧ (↑z : Int) = ↑x % ↑y := by
   apply Scalar.rem_unsigned_spec <;> simp [ScalarTy.isSigned, *]
 
 @[pspec] theorem I8.rem_spec (x : I8) {y : I8}
   (hnz : ↑y ≠ (0 : Int))
   (hmin : I8.min ≤ scalar_rem ↑x ↑y)
   (hmax : scalar_rem ↑x ↑y ≤ I8.max):
-  ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
+  ∃ z, x % y = ok z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
   Scalar.rem_spec hnz hmin hmax
 
 @[pspec] theorem I16.rem_spec (x : I16) {y : I16}
   (hnz : ↑y ≠ (0 : Int))
   (hmin : I16.min ≤ scalar_rem ↑x ↑y)
   (hmax : scalar_rem ↑x ↑y ≤ I16.max):
-  ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
+  ∃ z, x % y = ok z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
   Scalar.rem_spec hnz hmin hmax
 
 @[pspec] theorem I32.rem_spec (x : I32) {y : I32}
   (hnz : ↑y ≠ (0 : Int))
   (hmin : I32.min ≤ scalar_rem ↑x ↑y)
   (hmax : scalar_rem ↑x ↑y ≤ I32.max):
-  ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
+  ∃ z, x % y = ok z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
   Scalar.rem_spec hnz hmin hmax
 
 @[pspec] theorem I64.rem_spec (x : I64) {y : I64}
   (hnz : ↑y ≠ (0 : Int))
   (hmin : I64.min ≤ scalar_rem ↑x ↑y)
   (hmax : scalar_rem ↑x ↑y ≤ I64.max):
-  ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
+  ∃ z, x % y = ok z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
   Scalar.rem_spec hnz hmin hmax
 
 @[pspec] theorem I128.rem_spec (x : I128) {y : I128}
   (hnz : ↑y ≠ (0 : Int))
   (hmin : I128.min ≤ scalar_rem ↑x ↑y)
   (hmax : scalar_rem ↑x ↑y ≤ I128.max):
-  ∃ z, x % y = ret z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
+  ∃ z, x % y = ok z ∧ (↑z : Int) = scalar_rem ↑x ↑y :=
   Scalar.rem_spec hnz hmin hmax
 
 -- ofIntCore
@@ -1148,19 +1157,19 @@ theorem Scalar.eq_equiv {ty : ScalarTy} (x y : Scalar ty) :
 
 -- This is sometimes useful when rewriting the goal with the local assumptions
 @[simp] theorem Scalar.eq_imp {ty : ScalarTy} (x y : Scalar ty) :
-  x = y → (↑x : Int) = ↑y := (eq_equiv x y).mp
+  (↑x : Int) = ↑y → x = y := (eq_equiv x y).mpr
 
 theorem Scalar.lt_equiv {ty : ScalarTy} (x y : Scalar ty) :
   x < y ↔ (↑x : Int) < ↑y := by simp [LT.lt]
 
 @[simp] theorem Scalar.lt_imp {ty : ScalarTy} (x y : Scalar ty) :
-  x < y → (↑x : Int) < ↑y := (lt_equiv x y).mp
+  (↑x : Int) < (↑y) → x < y := (lt_equiv x y).mpr
 
 theorem Scalar.le_equiv {ty : ScalarTy} (x y : Scalar ty) :
   x ≤ y ↔ (↑x : Int) ≤ ↑y := by simp [LE.le]
 
 @[simp] theorem Scalar.le_imp {ty : ScalarTy} (x y : Scalar ty) :
-  x ≤ y → (↑x : Int) ≤ ↑y := (le_equiv x y).mp
+  (↑x : Int) ≤ ↑y → x ≤ y := (le_equiv x y).mpr
 
 instance Scalar.decLt {ty} (a b : Scalar ty) : Decidable (LT.lt a b) := Int.decLt ..
 instance Scalar.decLe {ty} (a b : Scalar ty) : Decidable (LE.le a b) := Int.decLe ..
@@ -1181,6 +1190,6 @@ instance (ty : ScalarTy) : DecidableEq (Scalar ty) :=
     | isFalse h => isFalse (Scalar.ne_of_val_ne h)
 
 @[simp] theorem Scalar.neq_to_neq_val {ty} : ∀ {i j : Scalar ty}, (¬ i = j) ↔ ¬ i.val = j.val := by
-  intro i j; cases i; cases j; simp
+  simp [eq_equiv]
 
 end Primitives
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index 65249c12..8e2d65a8 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -2,7 +2,6 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 import Base.IList
 import Base.Primitives.Scalar
@@ -61,34 +60,34 @@ def Vec.push (α : Type u) (v : Vec α) (x : α) : Result (Vec α)
       simp [Usize.max] at *
       have hm := Usize.refined_max.property
       cases h <;> cases hm <;> simp [U32.max, U64.max] at * <;> try linarith
-    return ⟨ List.concat v.val x, by simp at *; assumption ⟩
+    ok ⟨ List.concat v.val x, by simp at *; assumption ⟩
   else
     fail maximumSizeExceeded
 
 -- This shouldn't be used
 def Vec.insert_fwd (α : Type u) (v: Vec α) (i: Usize) (_: α) : Result Unit :=
   if i.val < v.length then
-    .ret ()
+    ok ()
   else
-    .fail arrayOutOfBounds
+    fail arrayOutOfBounds
 
 -- This is actually the backward function
 def Vec.insert (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
   if i.val < v.length then
-    .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
+    ok ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
   else
-    .fail arrayOutOfBounds
+    fail arrayOutOfBounds
 
 @[pspec]
 theorem Vec.insert_spec {α : Type u} (v: Vec α) (i: Usize) (x: α)
   (hbound : i.val < v.length) :
-  ∃ nv, v.insert α i x = ret nv ∧ nv.val = v.val.update i.val x := by
+  ∃ nv, v.insert α i x = ok nv ∧ nv.val = v.val.update i.val x := by
   simp [insert, *]
 
 def Vec.index_usize {α : Type u} (v: Vec α) (i: Usize) : Result α :=
   match v.val.indexOpt i.val with
   | none => fail .arrayOutOfBounds
-  | some x => ret x
+  | some x => ok x
 
 /- In the theorems below: we don't always need the `∃ ..`, but we use one
    so that `progress` introduces an opaque variable and an equality. This
@@ -98,7 +97,7 @@ def Vec.index_usize {α : Type u} (v: Vec α) (i: Usize) : Result α :=
 @[pspec]
 theorem Vec.index_usize_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
   (hbound : i.val < v.length) :
-  ∃ x, v.index_usize i = ret x ∧ x = v.val.index i.val := by
+  ∃ x, v.index_usize i = ok x ∧ x = v.val.index i.val := by
   simp only [index_usize]
   -- TODO: dependent rewrite
   have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
@@ -108,12 +107,12 @@ def Vec.update_usize {α : Type u} (v: Vec α) (i: Usize) (x: α) : Result (Vec
   match v.val.indexOpt i.val with
   | none => fail .arrayOutOfBounds
   | some _ =>
-    .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
+    ok ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
 
 @[pspec]
 theorem Vec.update_usize_spec {α : Type u} (v: Vec α) (i: Usize) (x : α)
   (hbound : i.val < v.length) :
-  ∃ nv, v.update_usize i x = ret nv ∧
+  ∃ nv, v.update_usize i x = ok nv ∧
   nv.val = v.val.update i.val x
   := by
   simp only [update_usize]
@@ -125,15 +124,15 @@ theorem Vec.update_usize_spec {α : Type u} (v: Vec α) (i: Usize) (x : α)
 def Vec.index_mut_usize {α : Type u} (v: Vec α) (i: Usize) :
   Result (α × (α → Result (Vec α))) :=
   match Vec.index_usize v i with
-  | ret x =>
-    ret (x, Vec.update_usize v i)
+  | ok x =>
+    ok (x, Vec.update_usize v i)
   | fail e => fail e
   | div => div
 
 @[pspec]
 theorem Vec.index_mut_usize_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
   (hbound : i.val < v.length) :
-  ∃ x back, v.index_mut_usize i = ret (x, back) ∧
+  ∃ x back, v.index_mut_usize i = ok (x, back) ∧
   x = v.val.index i.val ∧
   -- Backward function
   back = v.update_usize i
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index dc30c441..ea38c630 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -136,7 +136,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
     let _ ←
       tryTac
         (simpAt true []
-               [``Primitives.bind_tc_ret, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
+               [``Primitives.bind_tc_ok, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
                [hEq.fvarId!] (.targets #[] true))
     -- It may happen that at this point the goal is already solved (though this is rare)
     -- TODO: not sure this is the best way of checking it
@@ -397,33 +397,33 @@ namespace Test
   example {ty} {x y : Scalar ty}
     (hmin : Scalar.min ty ≤ x.val + y.val)
     (hmax : x.val + y.val ≤ Scalar.max ty) :
-    ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+    ∃ z, x + y = ok z ∧ z.val = x.val + y.val := by
     progress keep _ as ⟨ z, h1 .. ⟩
     simp [*, h1]
 
   example {ty} {x y : Scalar ty}
     (hmin : Scalar.min ty ≤ x.val + y.val)
     (hmax : x.val + y.val ≤ Scalar.max ty) :
-    ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+    ∃ z, x + y = ok z ∧ z.val = x.val + y.val := by
     progress keep h with Scalar.add_spec as ⟨ z ⟩
     simp [*, h]
 
   example {x y : U32}
     (hmax : x.val + y.val ≤ U32.max) :
-    ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+    ∃ z, x + y = ok z ∧ z.val = x.val + y.val := by
     -- This spec theorem is suboptimal, but it is good to check that it works
     progress with Scalar.add_spec as ⟨ z, h1 .. ⟩
     simp [*, h1]
  
   example {x y : U32}
     (hmax : x.val + y.val ≤ U32.max) :
-    ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+    ∃ z, x + y = ok z ∧ z.val = x.val + y.val := by
     progress with U32.add_spec as ⟨ z, h1 .. ⟩
     simp [*, h1]
 
   example {x y : U32}
     (hmax : x.val + y.val ≤ U32.max) :
-    ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+    ∃ z, x + y = ok z ∧ z.val = x.val + y.val := by
     progress keep _ as ⟨ z, h1 .. ⟩
     simp [*, h1]
 
@@ -431,7 +431,7 @@ namespace Test
      `α : Type u` where u is quantified, while here we use `α : Type 0` -/
   example {α : Type} (v: Vec α) (i: Usize) (x : α)
     (hbounds : i.val < v.length) :
-    ∃ nv, v.update_usize i x = ret nv ∧
+    ∃ nv, v.update_usize i x = ok nv ∧
     nv.val = v.val.update i.val x := by
     progress
     simp [*]
@@ -443,8 +443,8 @@ namespace Test
       (do
          (do
             let _ ← v.update_usize i x
-            .ret ())
-         .ret ()) = ret nv
+            .ok ())
+         .ok ()) = ok nv
       := by
     progress
     simp [*]
@@ -454,8 +454,8 @@ namespace Test
      not a constant. We also test the case where the function under scrutinee
      is not a constant. -/
   example {x : U32}
-    (f : U32 → Result Unit) (h : ∀ x, f x = .ret ()) :
-    f x = ret () := by
+    (f : U32 → Result Unit) (h : ∀ x, f x = .ok ()) :
+    f x = ok () := by
     progress
 
 end Test
diff --git a/backends/lean/lake-manifest.json b/backends/lean/lake-manifest.json
index 3a18466f..99ec856e 100644
--- a/backends/lean/lake-manifest.json
+++ b/backends/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": "056cc4b21e25e8d1daaeef3a6e3416872c9fc12c",
+   "rev": "3e99b48baf21ffdd202d5c2e39990fc23f4c6d32",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
diff --git a/backends/lean/lean-toolchain b/backends/lean/lean-toolchain
index f96d662e..9ad30404 100644
--- a/backends/lean/lean-toolchain
+++ b/backends/lean/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.6.1
+leanprover/lean4:v4.7.0