diff options
| author | Son Ho | 2023-10-25 18:44:28 +0200 |
|---|---|---|
| committer | Son Ho | 2023-10-25 18:44:28 +0200 |
| commit | 81b7a7d706bc1a0f2f57bc254a8af158039a10cf (patch) | |
| tree | 64ac32b95e61f12d54be54827a3efc66f829106f /backends/lean/Base/Progress | |
| parent | 862c6f939b001e4fe0556cc73af71210e7b96ea2 (diff) | |
Make the hashmap files typecheck again in Lean
Diffstat (limited to '')
| -rw-r--r-- | backends/lean/Base/Progress/Progress.lean | 3 |
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 [*] |