From af2968541eafc8c881ac5099031a2ddd8a02d686 Mon Sep 17 00:00:00 2001
From: Moritz Firsching <firsching@google.com>
Date: Tue, 19 May 2026 21:01:55 +0200
Subject: [PATCH] use String.toName

---
 Main.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Main.lean b/Main.lean
index 806fcf7..b835018 100644
--- a/Main.lean
+++ b/Main.lean
@@ -5,7 +5,7 @@ def main (args : List String) : IO Unit := do
   initSearchPath (← findSysroot)
   let (opts, args) := args.partition (fun s => s.startsWith "--" && s.length ≥ 3)
   let (imports, constants) := args.span (· != "--")
-  let imports := imports.toArray.map fun mod => { module := Syntax.decodeNameLit ("`" ++ mod) |>.get! }
+  let imports := imports.toArray.map fun mod => { module := mod.toName }
   let env ← importModules imports {}
   let constants := match constants.tail? with
     | some cs => cs.map fun c => Syntax.decodeNameLit ("`" ++ c) |>.get!