diff options
| author | Son Ho | 2023-08-04 20:02:37 +0200 |
|---|---|---|
| committer | Son Ho | 2023-08-04 20:02:37 +0200 |
| commit | c656688ff4895904b4bb5e2f89037f1e75c9fa00 (patch) | |
| tree | 5c2567513ebde16c11dd42ea60a679dcceb9bf4a /backends | |
| parent | 79225e6ca645ca3902b3b761966dc869306cedbd (diff) | |
Make minor modifications
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/lean/Base/Primitives/Vec.lean | 8 |
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 [*] |