From d7001c1b28b2f693ba0a4fb0c9f0533e267104af Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 24 Jun 2025 15:11:51 -0700 Subject: [PATCH] chore: Tomogram stub --- Tomogram.lean | 3 +++ lakefile.lean | 8 ++++++++ 2 files changed, 11 insertions(+) create mode 100644 Tomogram.lean 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 {