From 1a9e4500662318773d80e0e6845bc9e5ea3a5921 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 24 Jun 2025 15:23:59 -0700 Subject: [PATCH] refactor: Rename `tomogram` to `tomograph` --- Tomogram.lean | 3 --- Tomograph.lean | 5 +++++ lakefile.lean | 4 ++-- 3 files changed, 7 insertions(+), 5 deletions(-) delete mode 100644 Tomogram.lean create mode 100644 Tomograph.lean 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 }