Setup to transition to lean 4.

finite-set-exercises
Joshua Potter 2023-02-10 09:12:25 -07:00
parent 9d1f3120c1
commit e18b705ad3
6 changed files with 23 additions and 11 deletions

5
.gitignore vendored
View File

@ -1,3 +1,2 @@
*.olean
/_target
/leanpkg.path
/build
/lake-packages/*

1
Bookshelf.lean Normal file
View File

@ -0,0 +1 @@
def hello := "world"

4
Main.lean Normal file
View File

@ -0,0 +1,4 @@
import «Bookshelf»
def main : IO Unit :=
IO.println s!"Hello, {hello}!"

15
lakefile.lean Normal file
View File

@ -0,0 +1,15 @@
import Lake
open Lake DSL
package «bookshelf» {
-- add package configuration options here
}
lean_lib «Bookshelf» {
-- add library configuration options here
}
@[default_target]
lean_exe «bookshelf» {
root := `Main
}

1
lean-toolchain Normal file
View File

@ -0,0 +1 @@
leanprover/lean4:nightly-2023-02-10

View File

@ -1,8 +0,0 @@
[package]
name = "bookshelf"
version = "0.1"
lean_version = "leanprover-community/lean:3.50.3"
path = "src"
[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "4c19a16e4b705bf135cf9a80ac18fcc99c438514"}