sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity
39,750 Commits 4,240 Branches 120 Tags
joachim/compress-discrtree
Go to file
Clone
Open with VS Code Open with VSCodium Open with Intellij IDEA
Download ZIP Download TAR.GZ Download BUNDLE
Joachim Breitner f82aa9aedf refactor: path compression for DiscrTree 
This PR adds path compression to the DiscrTree trie data structure.
Instead of a single `.node` constructor, the `Trie` type now has four
constructors: `.empty`, `.values`, `.path` (for compressed sequences of
keys with no branching), and `.branch`. This significantly reduces the
size and maximum depth of large discrimination trees.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
2026-03-07 16:09:44 +00:00
.claude
chore: improve CI failure reporting in release checklist (#12786)
2026-03-04 11:55:34 +00:00
.github
fix: use pull_request_target for label-triggered workflows (#12638)
2026-03-01 19:20:56 +11:00
.vscode
chore: replace workspace file with .vscode/ settings (#12770)
2026-03-04 01:10:04 +00:00
doc
chore: replace workspace file with .vscode/ settings (#12770)
2026-03-04 01:10:04 +00:00
images
…
releases_drafts
chore: remove stale release draft notes (#12518)
2026-02-17 19:56:23 +00:00
script
fix: handle CACHE STRING syntax in LEAN_VERSION_IS_RELEASE check (#12800)
2026-03-05 02:09:51 +00:00
src
refactor: path compression for DiscrTree
2026-03-07 16:09:44 +00:00
stage0
refactor: path compression for DiscrTree
2026-03-07 16:09:44 +00:00
tests
refactor: path compression for DiscrTree
2026-03-07 16:09:44 +00:00
.gitattributes
doc: grove: update and add String data (#11551)
2025-12-08 16:49:37 +00:00
.gitignore
chore: replace workspace file with .vscode/ settings (#12770)
2026-03-04 01:10:04 +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
chore: ignore stage0/ (for rg etc.)
2022-03-18 15:28:20 +01:00
CMakeLists.txt
chore: fail build on non-make generators (#12690)
2026-02-25 13:59:40 +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
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
chore: relative lean-toolchains (#12652)
2026-02-25 10:23:35 +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.

Reference in New Issue View Git Blame Copy Permalink
Description
No description provided
leanlean4
Readme 5 GiB
Languages
Lean 94.3%
C++ 4.1%
Python 0.6%
Shell 0.4%
CMake 0.3%