From e3cb3646bbe3d50240aa0bf4763f8e816fb9a706 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 25 Oct 2023 15:36:06 +0200
Subject: Fix some issues at extraction and add builtins

---
 backends/lean/Base/Primitives/Vec.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'backends/lean/Base/Primitives/Vec.lean')

diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index c4c4d9f2..99fcedc6 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -6,7 +6,7 @@ import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 import Base.IList
 import Base.Primitives.Scalar
-import Base.Primitives.Array
+import Base.Primitives.ArraySlice
 import Base.Arith
 import Base.Progress.Base
 
-- 
cgit v1.2.3