commit 6c93d38e81cd0305128cde9ac1bd32d74e3367bd Author: mehbark Date: Tue Apr 8 12:39:09 2025 -0400 initial 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