max/lean4-htt

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

Find a file

David Thrane Christiansen 974fdd85c4 chore: enable `let rec` tactic completion and docs (#12072 ) This PR enables tactic completion and docs for the `let rec` tactic, which required a stage0 update after #12047.		2026-01-20 13:17:08 +00:00
.claude	chore: add CI log retrieval guidance to CLAUDE.md (#11964 )	2026-01-10 07:41:41 +00:00
.github	perf: avoid allocation on `lean_trace` use in interpreter (#12036 )	2026-01-18 19:33:48 +00:00
doc	doc: write a guideline for tactic docstrings (#11406 )	2026-01-06 04:40:20 +00:00
images
releases_drafts	chore: add release draft for the module system (#11359 )	2025-11-26 15:01:07 +00:00
script	feat: add `lake shake` command (#11921 )	2026-01-19 11:11:13 +00:00
src	chore: enable `let rec` tactic completion and docs (#12072 )	2026-01-20 13:17:08 +00:00
stage0	chore: update stage0	2026-01-20 12:05:41 +00:00
tests	chore: enable `let rec` tactic completion and docs (#12072 )	2026-01-20 13:17:08 +00:00
.gitattributes	doc: grove: update and add `String` data (#11551 )	2025-12-08 16:49:37 +00:00
.gitignore
.gitpod.Dockerfile
.gitpod.yml
.ignore
CMakeLists.txt	fix: cadical dynamic dependencies (#11475 )	2025-12-02 13:54:26 +00:00
CMakePresets.json	chore: CI: enable leak sanitizer again (#11339 )	2025-11-27 18:32:35 +00:00
CODEOWNERS
CONTRIBUTING.md
flake.lock
flake.nix
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
RELEASES.md

This is the repository for Lean 4.

About

Installation