summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Progress
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean/Base/Progress')
-rw-r--r--backends/lean/Base/Progress/Progress.lean3
1 files changed, 2 insertions, 1 deletions
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index ecf05dab..24c6f912 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -383,6 +383,7 @@ namespace Test
-- #eval showStoredPSpec
-- #eval showStoredPSpecClass
-- #eval showStoredPSpecExprClass
+ open alloc.vec
example {ty} {x y : Scalar ty}
(hmin : Scalar.min ty ≤ x.val + y.val)
@@ -408,7 +409,7 @@ namespace Test
`α : Type u` where u is quantified, while here we use `α : Type 0` -/
example {α : Type} (v: Vec α) (i: Usize) (x : α)
(hbounds : i.val < v.length) :
- ∃ nv, v.index_mut_back α i x = ret nv ∧
+ ∃ nv, v.update_usize α i x = ret nv ∧
nv.val = v.val.update i.val x := by
progress
simp [*]