diff --git a/Tomogram.lean b/Tomogram.lean deleted file mode 100644 index 3936e71..0000000 --- a/Tomogram.lean +++ /dev/null @@ -1,3 +0,0 @@ - -def main : IO Unit := do - IO.println "tomogram stub" diff --git a/Tomograph.lean b/Tomograph.lean new file mode 100644 index 0000000..0878b36 --- /dev/null +++ b/Tomograph.lean @@ -0,0 +1,5 @@ + + +def main (args : List String) : IO Unit := do + let command :: args := args | IO.eprintln "Must supply a command" + IO.println s!"{command}" diff --git a/lakefile.lean b/lakefile.lean index 5cfaf87..194fbfc 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -19,8 +19,8 @@ lean_exe repl { } @[default_target] -lean_exe tomogram { - root := `Tomogram +lean_exe tomograph { + root := `Tomograph -- Solves the native symbol not found problem supportInterpreter := true }