14 lines
316 B
Text
14 lines
316 B
Text
|
import «Lean4CliExample»
|
||
|
|
|
||
|
|
/---
|
||
|
|
Main entry
|
||
|
|
--/
|
||
|
|
def main (args: List String) : IO UInt32 :=
|
||
|
|
exampleCmd.validate args
|
||
|
|
|
||
|
|
#eval main <| "-i -o -p 1 --module=Lean.Compiler --set-paths=path1,path2,path3 input output1 output2".splitOn " "
|
||
|
|
|
||
|
|
#eval main <| "-io -p1 input".splitOn " "
|
||
|
|
|
||
|
|
#eval main <| "--version".splitOn " "
|