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.
33584 commits 1 branch 0 tags 5.3 GiB
Find a file
Kyle Miller 95bf6793aa
fix: make cdot anonymous function notation handle ambiguous notation (#4833) 
Fixes an issue where each alternative in choice nodes would get their
own arguments. Now cdot function expansion is aware of choice nodes.

Also modifies the variable naming so that multi-argument functions like
`(· + ·)` expand as `fun x1 x2 => x1 + x2` rather than `fun x x_1 => x +
x_1`.

Closes #4832
2024-08-09 21:16:51 +00:00
.github chore: CI: remove rebase command 2024-08-08 11:17:52 +02:00
doc chore: add parallelism fallback for macOS on build (#4647) 2024-08-08 14:26:06 +00:00
images
nix chore: deprecate Nix-based build, remove interactive components (#4895) 2024-08-02 09:57:34 +00:00
releases_drafts chore: copy release notes from releases/v4.10.0 (#4864) 2024-07-31 03:30:13 +00:00
script feat: support Lake for building Lean core oleans (#3886) 2024-06-13 16:18:24 +00:00
src fix: make cdot anonymous function notation handle ambiguous notation (#4833) 2024-08-09 21:16:51 +00:00
stage0 chore: update stage0 2024-08-09 16:16:48 +00:00
tests fix: make cdot anonymous function notation handle ambiguous notation (#4833) 2024-08-09 21:16:51 +00:00
.gitattributes chore: Do not hide stage0/src/stdlib_flags.h from diffs 2023-09-13 19:29:25 +02:00
.gitignore feat: support Lake for building Lean core oleans (#3886) 2024-06-13 16:18:24 +00:00
.ignore chore: ignore stage0/ (for rg etc.) 2022-03-18 15:28:20 +01:00
CMakeLists.txt chore: update-stage0-commit cmake target (#3692) 2024-04-04 13:35:53 +00:00
CMakePresets.json chore: modernize build instructions (#4032) 2024-05-23 10:55:07 +00:00
CODEOWNERS chore: update codeowners (#4681) 2024-07-08 07:57:54 +00:00
CONTRIBUTING.md doc: triage 2024-07-26 18:24:06 +02:00
flake.lock chore: deprecate Nix-based build, remove interactive components (#4895) 2024-08-02 09:57:34 +00:00
flake.nix chore: deprecate Nix-based build, remove interactive components (#4895) 2024-08-02 09:57:34 +00:00
lean-toolchain doc: VS Code dev setup (#2961) 2023-11-30 08:35:03 +00:00
lean.code-workspace chore: add the lean4 extension to the vscode workspace (#3059) 2023-12-14 08:58:21 +00:00
LICENSE chore: remove LICENSE header that confused GitHub 2021-11-18 09:42:35 +01:00
LICENSES chore: add GMP license for now 2021-11-18 09:42:35 +01:00
README.md doc: mention build doc source location (#4045) 2024-05-01 22:42:54 +00:00
RELEASES.md chore: copy release notes from releases/v4.10.0 (#4864) 2024-07-31 03:30:13 +00:00

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean (documentation source: doc/make/index.md).