From f35aba375757db99d2dc6ac2b11b9eb1e437b420 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 24 Oct 2023 11:58:35 +0200
Subject: Add definitions in for the Lean Primitives library

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

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

diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean
index 6b7b0792..22378af7 100644
--- a/backends/lean/Base/Primitives.lean
+++ b/backends/lean/Base/Primitives.lean
@@ -2,3 +2,5 @@ import Base.Primitives.Base
 import Base.Primitives.Scalar
 import Base.Primitives.Array
 import Base.Primitives.Vec
+import Base.Primitives.Alloc
+import Base.Primitives.CoreOpsDeref
-- 
cgit v1.2.3


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.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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

diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean
index 22378af7..613b6076 100644
--- a/backends/lean/Base/Primitives.lean
+++ b/backends/lean/Base/Primitives.lean
@@ -1,6 +1,6 @@
 import Base.Primitives.Base
 import Base.Primitives.Scalar
-import Base.Primitives.Array
+import Base.Primitives.ArraySlice
 import Base.Primitives.Vec
 import Base.Primitives.Alloc
-import Base.Primitives.CoreOpsDeref
+import Base.Primitives.CoreOps
-- 
cgit v1.2.3