From 7fb44aed84b96c0b4bc7b80946c4903e3a3e8923 Mon Sep 17 00:00:00 2001 From: Abdalrhman M Mohamed Date: Sun, 27 Oct 2024 16:20:37 -0700 Subject: [PATCH] chore: delete debug print statement --- Main.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Main.lean b/Main.lean index 2629135..305571b 100644 --- a/Main.lean +++ b/Main.lean @@ -65,7 +65,7 @@ def elabParseAndDecideSmt2File (path : System.FilePath) : CommandElabM Unit := d def parseOptions (args : List String) : IO (Options × List String) := do let (opts, args) := go {} args - return (← Lean.Language.Lean.reparseOptions opts, args) + return (← Language.Lean.reparseOptions opts, args) where go (opts : Options) : List String → (Options × List String) | "-D" :: arg :: args => @@ -79,7 +79,6 @@ where unsafe def main (args : List String) : IO Unit := do Lean.initSearchPath (← Lean.findSysroot) let (opts, args) ← parseOptions args - IO.println opts let [path] := args | throw (.userError "usage: lake exe leanwuzla [-D name=value] /path/to/file.smt2") withImportModules #[`Std.Tactic.BVDecide] {} 0 fun env => do