summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean/Base/Primitives')
-rw-r--r--backends/lean/Base/Primitives/Vec.lean7
1 files changed, 2 insertions, 5 deletions
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index e584777a..12789fa9 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -48,10 +48,7 @@ abbrev Vec.len (α : Type u) (v : Vec α) : Usize :=
theorem Vec.len_val {α : Type u} (v : Vec α) : (Vec.len α v).val = v.length :=
by rfl
--- This shouldn't be used
-def Vec.push_fwd (α : Type u) (_ : Vec α) (_ : α) : Unit := ()
-
--- This is actually the backward function
+@[irreducible]
def Vec.push (α : Type u) (v : Vec α) (x : α) : Result (Vec α)
:=
let nlen := List.length v.val + 1
@@ -68,7 +65,7 @@ def Vec.push (α : Type u) (v : Vec α) (x : α) : Result (Vec α)
theorem Vec.push_spec {α : Type u} (v : Vec α) (x : α) (h : v.val.len < Usize.max) :
∃ v1, v.push α x = ok v1 ∧
v1.val = v.val ++ [x] := by
- simp [push]
+ rw [push]; simp
split <;> simp_all [List.len_eq_length]
scalar_tac