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.
38516 commits 1 branch 0 tags 5.3 GiB
Find a file
Kim Morrison 833aaa823e
chore: tactics using library suggestions set the caller field (#11171) 
This PR ensures that tactics using library suggestions set the caller
field, so the premise selection engine has access to this. We'll later
use this to filter out some modules for grind, which we know have
already been fully annotated.

Co-authored-by: Claude <noreply@anthropic.com>
2025-11-14 04:50:55 +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 feat: String.toList_map (#11021) 2025-11-01 13:54:39 +00:00
images
releases_drafts chore: updates to release_checklist.md (#7817) 2025-04-04 03:45:36 +00:00
script feat: #grind_lint command (#11157) 2025-11-13 00:42:18 +00:00
src chore: tactics using library suggestions set the caller field (#11171) 2025-11-14 04:50:55 +00:00
stage0 chore: update stage0 2025-11-13 02:05:09 +00:00
tests feat: add #grind_lint check in module <module> (#11167) 2025-11-14 01:44:04 +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 doc: VS Code dev setup (#2961) 2023-11-30 08:35:03 +00:00
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.