From 836a14fa6396c7af6375b1bc9e4c653ed19ef5e3 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 5 Oct 2023 17:49:43 -0700
Subject: [PATCH] Bump Lean version to 4.1.0

---
 .gitignore     | 1 +
 Main.lean      | 2 +-
 lean-toolchain | 2 +-
 3 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/.gitignore b/.gitignore
index 069f8e2..21bcd46 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,5 +1,6 @@
 .*
 !.gitignore
 
+*.olean
 /build
 /lake-packages
diff --git a/Main.lean b/Main.lean
index dc4b14f..8fd617b 100644
--- a/Main.lean
+++ b/Main.lean
@@ -88,7 +88,7 @@ unsafe def main (args: List String): IO Unit := do
   let imports:= args.filter (λ s => ¬ (s.startsWith "--"))
 
   let env ← Lean.importModules
-    (imports := imports.map (λ str => { module := str_to_name str, runtimeOnly := false }))
+    (imports := imports.toArray.map (λ str => { module := str_to_name str, runtimeOnly := false }))
     (opts := {})
     (trustLevel := 1)
   let context: Context := {
diff --git a/lean-toolchain b/lean-toolchain
index 49fd71c..a9bddf0 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:4.0.0
+leanprover/lean4:4.1.0