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.
39940 commits 1 branch 0 tags 5.3 GiB
Find a file
Henrik Böving 08595c5f8f
fix: interaction of extern annotations and calls to functions with borrowed parameters (#13052) 
This PR fixes a bug in the borrow inference in connection with `export`
annotations.

Previously parameters of `export` functions were presumed as owned from
the beginning of the
analysis. However, they were not added into the set of owned parameters
and thus sometimes failed to
force necessary changes to borrowedness of other values that the
parameters flowed into.
2026-03-23 10:03:26 +00:00
.claude chore: speed up test suite slightly (#12969) 2026-03-20 12:24:32 +00:00
.github chore: CI: bump git cache to 5GB (#13053) 2026-03-23 08:58:35 +00:00
.vscode chore: replace workspace file with .vscode/ settings (#12770) 2026-03-04 01:10:04 +00:00
doc feat: unfold and rewrap instances in inferInstanceAs and deriving 2026-03-22 13:25:46 +01:00
images
releases_drafts chore: remove stale release draft notes (#12518) 2026-02-17 19:56:23 +00:00
script fix: handle lean4-nightly toolchain prefix in release checklist (#12865) 2026-03-23 03:01:58 +00:00
src fix: interaction of extern annotations and calls to functions with borrowed parameters (#13052) 2026-03-23 10:03:26 +00:00
stage0 chore: update stage0 2026-03-22 13:25:46 +01:00
tests feat: simproc for turning "c" into String.singleton 'c' (#13054) 2026-03-23 09:06:49 +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 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 leantar available in stage0 (#12992) 2026-03-19 20:43:43 +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 chore: migrate pkg tests (#12889) 2026-03-11 18:55:46 +00:00
flake.lock chore: update to c++20 (#12117) 2026-02-11 01:17:40 +00:00
flake.nix chore: add aarch64-darwin to flake (#12915) 2026-03-18 15:55:34 +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.