summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives
diff options
context:
space:
mode:
authorSon Ho2023-08-04 20:02:37 +0200
committerSon Ho2023-08-04 20:02:37 +0200
commitc656688ff4895904b4bb5e2f89037f1e75c9fa00 (patch)
tree5c2567513ebde16c11dd42ea60a679dcceb9bf4a /backends/lean/Base/Primitives
parent79225e6ca645ca3902b3b761966dc869306cedbd (diff)
Make minor modifications
Diffstat (limited to 'backends/lean/Base/Primitives')
-rw-r--r--backends/lean/Base/Primitives/Vec.lean8
1 files changed, 4 insertions, 4 deletions
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index d37fb5fd..c4c4d9f2 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -79,7 +79,7 @@ theorem Vec.insert_spec {α : Type u} (v: Vec α) (i: Usize) (x: α)
∃ nv, v.insert α i x = ret nv ∧ nv.val = v.val.update i.val x := by
simp [insert, *]
-def Vec.index (α : Type u) (v: Vec α) (i: Usize) : Result α :=
+def Vec.index_shared (α : Type u) (v: Vec α) (i: Usize) : Result α :=
match v.val.indexOpt i.val with
| none => fail .arrayOutOfBounds
| some x => ret x
@@ -90,10 +90,10 @@ def Vec.index (α : Type u) (v: Vec α) (i: Usize) : Result α :=
-/
@[pspec]
-theorem Vec.index_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
+theorem Vec.index_shared_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
(hbound : i.val < v.length) :
- ∃ x, v.index α i = ret x ∧ x = v.val.index i.val := by
- simp only [index]
+ ∃ x, v.index_shared α i = ret x ∧ x = v.val.index i.val := by
+ simp only [index_shared]
-- TODO: dependent rewrite
have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
simp [*]