From acc09d5c69690f2c46cb1bacf290da5dcc268b24 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 6 Jun 2023 15:53:46 +0200
Subject: Remove the sorries from Primitives.lean

---
 backends/lean/lakefile.lean | 1 +
 1 file changed, 1 insertion(+)

(limited to 'backends/lean/lakefile.lean')

diff --git a/backends/lean/lakefile.lean b/backends/lean/lakefile.lean
index 9633e1e8..c5e27d1c 100644
--- a/backends/lean/lakefile.lean
+++ b/backends/lean/lakefile.lean
@@ -1,6 +1,7 @@
 import Lake
 open Lake DSL
 
+-- Important: mathlib imports std4 and quote4: we mustn't add a `require std4` line
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git"
 
-- 
cgit v1.2.3


From e2fef1a5c986aff4c9975b1376bcc0fc0bb87940 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 9 Jun 2023 10:06:43 +0200
Subject: Reorganize a bit the Lean library

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

(limited to 'backends/lean/lakefile.lean')

diff --git a/backends/lean/lakefile.lean b/backends/lean/lakefile.lean
index c5e27d1c..21a4a332 100644
--- a/backends/lean/lakefile.lean
+++ b/backends/lean/lakefile.lean
@@ -8,4 +8,4 @@ require mathlib from git
 package «base» {}
 
 @[default_target]
-lean_lib «Primitives» {}
+lean_lib «Base» {}
-- 
cgit v1.2.3