From 81b7a7d706bc1a0f2f57bc254a8af158039a10cf Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 25 Oct 2023 18:44:28 +0200
Subject: Make the hashmap files typecheck again in Lean

---
 backends/lean/Base/Progress/Progress.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'backends/lean/Base/Progress')

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 [*]
-- 
cgit v1.2.3