Skip to content

Commit

Permalink
chore: delete debug print statement
Browse files Browse the repository at this point in the history
  • Loading branch information
abdoo8080 committed Oct 27, 2024
1 parent 13a8403 commit 7fb44ae
Showing 1 changed file with 1 addition and 2 deletions.
3 changes: 1 addition & 2 deletions Main.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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 =>
Expand All @@ -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
Expand Down

0 comments on commit 7fb44ae

Please sign in to comment.