From 6c93d38e81cd0305128cde9ac1bd32d74e3367bd Mon Sep 17 00:00:00 2001 From: mehbark Date: Tue, 8 Apr 2025 12:39:09 -0400 Subject: [PATCH] initial --- Bytecode.lean | 3 +++ Bytecode/Basic.lean | 1 + Main.lean | 4 ++++ README.md | 1 + lakefile.toml | 10 ++++++++++ lean-toolchain | 1 + 6 files changed, 20 insertions(+) create mode 100644 Bytecode.lean create mode 100644 Bytecode/Basic.lean create mode 100644 Main.lean create mode 100644 README.md create mode 100644 lakefile.toml create mode 100644 lean-toolchain diff --git a/Bytecode.lean b/Bytecode.lean new file mode 100644 index 0000000..79c3282 --- /dev/null +++ b/Bytecode.lean @@ -0,0 +1,3 @@ +-- This module serves as the root of the `Bytecode` library. +-- Import modules here that should be built as part of the library. +import Bytecode.Basic diff --git a/Bytecode/Basic.lean b/Bytecode/Basic.lean new file mode 100644 index 0000000..99415d9 --- /dev/null +++ b/Bytecode/Basic.lean @@ -0,0 +1 @@ +def hello := "world" diff --git a/Main.lean b/Main.lean new file mode 100644 index 0000000..257b937 --- /dev/null +++ b/Main.lean @@ -0,0 +1,4 @@ +import Bytecode + +def main : IO Unit := + IO.println s!"Hello, {hello}!" diff --git a/README.md b/README.md new file mode 100644 index 0000000..9417fcb --- /dev/null +++ b/README.md @@ -0,0 +1 @@ +# bytecode \ No newline at end of file diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000..afcbbed --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,10 @@ +name = "bytecode" +version = "0.1.0" +defaultTargets = ["bytecode"] + +[[lean_lib]] +name = "Bytecode" + +[[lean_exe]] +name = "bytecode" +root = "Main" diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..a3edb8f --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.16.0-rc2