commit f25a2dda4e949fc02cc783b9e7056cd2193ba006 Author: Leopold Fajtak Date: Mon Sep 22 09:56:03 2025 +0200 Set up project diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml new file mode 100644 index 0000000..09cd4ca --- /dev/null +++ b/.github/workflows/lean_action_ci.yml @@ -0,0 +1,14 @@ +name: Lean Action CI + +on: + push: + pull_request: + workflow_dispatch: + +jobs: + build: + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v4 + - uses: leanprover/lean-action@v1 diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..bfb30ec --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +/.lake diff --git a/InductiveVerification.lean b/InductiveVerification.lean new file mode 100644 index 0000000..d9843f5 --- /dev/null +++ b/InductiveVerification.lean @@ -0,0 +1,3 @@ +-- This module serves as the root of the `InductiveVerification` library. +-- Import modules here that should be built as part of the library. +import InductiveVerification.Basic diff --git a/InductiveVerification/Basic.lean b/InductiveVerification/Basic.lean new file mode 100644 index 0000000..99415d9 --- /dev/null +++ b/InductiveVerification/Basic.lean @@ -0,0 +1 @@ +def hello := "world" diff --git a/Main.lean b/Main.lean new file mode 100644 index 0000000..9da78ea --- /dev/null +++ b/Main.lean @@ -0,0 +1,4 @@ +import InductiveVerification + +def main : IO Unit := + IO.println s!"Hello, {hello}!" diff --git a/README.md b/README.md new file mode 100644 index 0000000..a1136e3 --- /dev/null +++ b/README.md @@ -0,0 +1 @@ +# inductive-verification \ No newline at end of file diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000..a836890 --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,10 @@ +name = "inductive-verification" +version = "0.1.0" +defaultTargets = ["inductive-verification"] + +[[lean_lib]] +name = "InductiveVerification" + +[[lean_exe]] +name = "inductive-verification" +root = "Main" diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..7f254a9 --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.23.0