From 4828b77847ee981f5c6a1bbad7f8e6ed0e58eb0f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 16:08:32 +0200
Subject: Rename Result.ret as Result.ok in the backends

---
 backends/lean/Base/Primitives/Vec.lean | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

(limited to 'backends/lean/Base/Primitives/Vec.lean')

diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index 65249c12..dbe5c8dd 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -61,34 +61,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 +98,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 +108,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 +125,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
-- 
cgit v1.2.3