max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.
38355 commits 1 branch 0 tags 5.3 GiB
Find a file
Eric Wieser b3ef7c9f25
chore: add an assertion about mkValueTypeClosure (#10954) 
This is a guard against #10705; if a kernel error is raised when the
return value of this function is eventually checked, it is often
silenced downstream, making it hard to spot the failure.
If we panic here via `assert!`, then the diagnostic cannot be missed.
2025-10-25 12:59:17 +00:00
.claude/commands chore: updates to release automation (#10888) 2025-10-22 03:17:28 +00:00
.github chore: fix C++ warning (#10922) 2025-10-24 11:09:08 +00:00
doc feat: zero cost BaseIO (#10625) 2025-10-22 10:55:12 +02:00
images
releases_drafts chore: updates to release_checklist.md (#7817) 2025-04-04 03:45:36 +00:00
script chore: release_steps runs lake exe cache get when needed (#10882) 2025-10-21 22:49:38 +00:00
src chore: add an assertion about mkValueTypeClosure (#10954) 2025-10-25 12:59:17 +00:00
stage0 chore: update stage0 2025-10-25 11:32:01 +00:00
tests fix: bug in cutsat model construction (#10951) 2025-10-25 04:16:32 +00:00
.gitattributes fix: mark doc parser tests as eol=lf (#10344) 2025-09-11 11:19:01 +00:00
.gitignore chore: add .vscode/settings.json to .gitignore (#10795) 2025-10-16 07:08:41 +00:00
.gitpod.Dockerfile chore: add gitpod configuration (#6382) 2024-12-15 21:38:13 +00:00
.gitpod.yml chore: add gitpod configuration (#6382) 2024-12-15 21:38:13 +00:00
.ignore
CMakeLists.txt chore: make USE_LAKE the default (#10016) 2025-08-21 11:43:25 +00:00
CMakePresets.json chore: fix reldebug preset (#8051) 2025-04-23 10:05:11 +00:00
CODEOWNERS chore: make @hargoniX code owner of the compiler (#10732) 2025-10-10 04:43:38 +00:00
CONTRIBUTING.md doc: triage 2024-07-26 18:24:06 +02:00
flake.lock chore: robustify Nix shell (#8141) 2025-04-28 15:08:32 +00:00
flake.nix chore: use lld if available for building core (#10694) 2025-10-08 16:47:30 +00:00
lean-toolchain
lean.code-workspace chore: lean.code-workspace: fix terminal cwd (#10802) 2025-10-16 20:19:12 +00:00
LICENSE
LICENSES feat: ship cadical (#4325) 2024-08-23 09:13:27 +00:00
README.md doc: update URLs that are currently pointing to redirects (#10397) 2025-09-17 15:50:07 +00:00
RELEASES.md chore: updates to release_checklist.md (#7817) 2025-04-04 03:45:36 +00:00

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.