diff options
Diffstat (limited to 'backends/lean/Base')
| -rw-r--r-- | backends/lean/Base/Primitives/Vec.lean | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean index 4ecfa28f..be3a0e5b 100644 --- a/backends/lean/Base/Primitives/Vec.lean +++ b/backends/lean/Base/Primitives/Vec.lean @@ -38,7 +38,8 @@ def Vec.len (α : Type u) (v : Vec α) : Usize := let ⟨ v, l ⟩ := v Usize.ofIntCore (List.length v) (by simp [Scalar.min, Usize.min]) l -def Vec.length {α : Type u} (v : Vec α) : Int := v.val.len +@[simp] +abbrev Vec.length {α : Type u} (v : Vec α) : Int := v.val.len -- This shouldn't be used def Vec.push_fwd (α : Type u) (_ : Vec α) (_ : α) : Unit := () @@ -89,7 +90,7 @@ theorem Vec.index_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) : intro simp only [index] -- TODO: dependent rewrite - have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp[length] at *; simp [*]) + have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*]) simp only [*] -- This shouldn't be used @@ -111,13 +112,14 @@ theorem Vec.index_mut_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) : intro simp only [index_mut] -- TODO: dependent rewrite - have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp[length] at *; simp [*]) + have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*]) simp only [*] def Vec.index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) := match v.val.indexOpt i.val with | none => fail .arrayOutOfBounds | some _ => + -- TODO: int_tac: introduce the refinements in the context? .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩ @[pspec] |