max/lean4-htt

Fork 0

Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.

Find a file

Kim Morrison 26b435fa4d feat: `grind_pattern` for `Subtype.property` (#11317 ) This PR adds `grind_pattern Subtype.property => self.val`.		2025-11-22 02:23:09 +00:00
.claude	chore: basic dev instructions for Claude (#11074 )	2025-11-04 04:07:53 +00:00
.github	chore: CI: bump actions/upload-artifact from 4 to 5 (#11052 )	2025-11-11 12:41:14 +00:00
doc	fix: symbol clashes between packages (#11082 )	2025-11-19 02:24:44 +00:00
images
releases_drafts
script	test: re-enable re-elab benchmarks and add watchdog re-elab benchmark (#11284 )	2025-11-20 22:53:08 +00:00
src	feat: `grind_pattern` for `Subtype.property` (#11317 )	2025-11-22 02:23:09 +00:00
stage0	chore: update stage0	2025-11-21 19:35:21 +11:00
tests	feat: improve error message in the case of type class synthesis failure (#11245 )	2025-11-21 21:24:27 +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
.gitpod.yml
.ignore
CMakeLists.txt	chore: make `USE_LAKE` the default (#10016 )	2025-08-21 11:43:25 +00:00
CMakePresets.json
CODEOWNERS	chore: make @hargoniX code owner of the compiler (#10732 )	2025-10-10 04:43:38 +00:00
CONTRIBUTING.md
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
README.md	doc: update URLs that are currently pointing to redirects (#10397 )	2025-09-17 15:50:07 +00:00
RELEASES.md

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.