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.
39781 commits 1 branch 0 tags 5.3 GiB
Find a file
Henrik Böving 670360681f
perf: handle match_same_ctor.het similar to matchers in compiler (#12850) 
This PR optimizes the handling of `match_same_ctor.het` to make it emit
nice match trees as opposed to unoptimized CPS style code.

`match_same_ctor.het` is essentially a specialized kind of matcher where
we know that two objects are built from the same constructor and we wish
to call a continuation on their data. This means for every constructor
that contains data `het` takes one closure as an argument. Then after
matching on one of the objects every closure but the one relevant for
the match is released in every match arm, causing quadratic code
generation. This PR ensures that the `het` declarations get inlined and
then further processed by ordinary matcher and casesOn compilation,
thereby removing all of the continuations from the compiled code.
2026-03-09 22:02:06 +00:00
.claude chore: improve CI failure reporting in release checklist (#12786) 2026-03-04 11:55:34 +00:00
.github fix: address unused simp theorem warnings (#12829) 2026-03-06 23:12:03 +00:00
.vscode chore: replace workspace file with .vscode/ settings (#12770) 2026-03-04 01:10:04 +00:00
doc chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
images
releases_drafts chore: remove stale release draft notes (#12518) 2026-02-17 19:56:23 +00:00
script feat: unify name demangling with single Lean implementation (#12539) 2026-03-06 12:29:35 +00:00
src perf: handle match_same_ctor.het similar to matchers in compiler (#12850) 2026-03-09 22:02:06 +00:00
stage0 chore: turn on new do elaborator in Core (#12656) 2026-03-09 12:38:33 +00:00
tests perf: handle match_same_ctor.het similar to matchers in compiler (#12850) 2026-03-09 22:02:06 +00:00
.gitattributes chore: migrate more tests to new test suite (#12809) 2026-03-06 16:52:01 +00:00
.gitignore chore: replace workspace file with .vscode/ settings (#12770) 2026-03-04 01:10:04 +00:00
.gitpod.Dockerfile
.gitpod.yml
.ignore
CMakeLists.txt feat: bundle leantar with Lean (#12822) 2026-03-09 20:10:59 +00:00
CMakePresets.json chore: fix ci for new test suite (#12704) 2026-02-27 23:25:37 +00:00
CODEOWNERS chore: make @hargoniX code owner of the compiler (#10732) 2025-10-10 04:43:38 +00:00
CONTRIBUTING.md
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 chore: relative lean-toolchains (#12652) 2026-02-25 10:23:35 +00:00
LICENSE
LICENSES feat: bundle leantar with Lean (#12822) 2026-03-09 20:10:59 +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.