diff --git a/Tomogram.lean b/Tomogram.lean new file mode 100644 index 0000000..3936e71 --- /dev/null +++ b/Tomogram.lean @@ -0,0 +1,3 @@ + +def main : IO Unit := do + IO.println "tomogram stub" diff --git a/lakefile.lean b/lakefile.lean index ddf721a..5cfaf87 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -10,6 +10,7 @@ lean_lib Pantograph { lean_lib Repl { } + @[default_target] lean_exe repl { root := `Main @@ -17,6 +18,13 @@ lean_exe repl { supportInterpreter := true } +@[default_target] +lean_exe tomogram { + root := `Tomogram + -- Solves the native symbol not found problem + supportInterpreter := true +} + require LSpec from git "https://github.com/argumentcomputer/LSpec.git" @ "a6652a48b5c67b0d8dd3930fad6390a97d127e8d" lean_lib Test {