Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
Find a file
Henrik Böving c66cb00c0f
refactor: turn the AIG framework's RefVec from Array to Vector (#7603)
This PR uses the new `Vector` API inside of the AIG framework's `RefVec`
datatype.
2025-03-20 16:57:04 +00:00
.github chore: CI: USE_LAKE secondary build job (#7505) 2025-03-20 12:16:53 +00:00
doc
images
nix
releases chore: copy v4.17.0 release notes from releases/v4.17.0 branch (#7325) 2025-03-04 11:24:51 +00:00
releases_drafts
script fix: indenting in release notes script (#7326) 2025-03-12 23:02:02 +00:00
src refactor: turn the AIG framework's RefVec from Array to Vector (#7603) 2025-03-20 16:57:04 +00:00
stage0 chore: CI: USE_LAKE secondary build job (#7505) 2025-03-20 12:16:53 +00:00
tests feat: pretty printing structures, omit default values (#7589) 2025-03-20 15:32:13 +00:00
.gitattributes
.gitignore
.gitpod.Dockerfile
.gitpod.yml
.ignore
CMakeLists.txt chore: CI: USE_LAKE secondary build job (#7505) 2025-03-20 12:16:53 +00:00
CMakePresets.json
CODEOWNERS
CONTRIBUTING.md
flake.lock feat: upgrade cadical to 2.1.2 (#7347) 2025-03-05 17:58:58 +00:00
flake.nix feat: upgrade cadical to 2.1.2 (#7347) 2025-03-05 17:58:58 +00:00
lean-toolchain
lean.code-workspace
LICENSE
LICENSES
README.md
RELEASES.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean (documentation source: doc/make/index.md).