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.
39604 commits 1 branch 0 tags 5.3 GiB
Find a file
Leonardo de Moura 13a2a6b4c1
chore: update CLAUDE.md PR body formatting guidelines (#12629) 
This PR updates the CLAUDE.md instructions to better conform with our PR
conventions. Specifically, it clarifies that PR bodies must start with
"This PR" (which gets incorporated into release notes), and that
markdown headings like `## Summary` or `## Test plan` should not be used
in PR descriptions.

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
2026-02-20 18:53:18 +00:00
.claude chore: update CLAUDE.md PR body formatting guidelines (#12629) 2026-02-20 18:53:18 +00:00
.github feat: lazy initialization of closed terms (#12044) 2026-02-20 08:45:15 +00:00
doc chore: improve release command PR status checking (#12536) 2026-02-17 21:21:30 +00:00
images
releases_drafts chore: remove stale release draft notes (#12518) 2026-02-17 19:56:23 +00:00
script fix: update bump branch toolchain to nightly for all repos (#12586) 2026-02-19 13:04:26 +00:00
src fix: revert #12615 which broke Leroy's compiler verification course benchmark (#12627) 2026-02-20 17:54:52 +00:00
stage0 chore: update stage0 2026-02-20 13:32:43 +00:00
tests fix: revert #12615 which broke Leroy's compiler verification course benchmark (#12627) 2026-02-20 17:54:52 +00:00
.gitattributes doc: grove: update and add String data (#11551) 2025-12-08 16:49:37 +00:00
.gitignore chore: enable leanprover/skills plugin for Claude Code (#12609) 2026-02-20 12:35:32 +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: fix repeated cmake calls breaking the build (#12598) 2026-02-19 16:23:47 +00:00
CMakePresets.json chore: CI: enable leak sanitizer again (#11339) 2025-11-27 18:32:35 +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: update to c++20 (#12117) 2026-02-11 01:17:40 +00:00
flake.nix chore: update to c++20 (#12117) 2026-02-11 01:17:40 +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.