A Lean 4 adaptation of the Software Foundations series by Benjamin Pierce et al.
- Software Foundations
- Lean 4 and nightly releases.
- Lake: build system and package manager for Lean 4; the Lean 4 counterpart of Rust's "cargo".
- Lean Manual
- Theorem Proving in Lean
- Functional Programming in Lean
- Package
std: standard library for Lean 4. - Package
mathlib: mathematical libarary for Lean 4.
elan self update
elan update
elan default leanprover/lean4:nightly
elan toolchain list
## leanprover/lean4:nightly (default)
lake --version
## Lake version 4.1.0-pre (Lean version 4.0.0-nightly-2023-05-09)
lake init software-foundations
## lean-toolchain: "leanprover/lean4:nightly-2023-05-09"
# Build and run the target binary `grader`:
lake exe grader