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.
32776 commits 1 branch 0 tags 5.3 GiB
Find a file
Mario Carneiro ddbdfb954b
chore: use Ordering.then in deriving Ord (#3893) 
This should improve the performance of the deriving a bit since it
doesn't have to generate so many matchers. The main motivation though is
to make it easier to prove properties about the expression by using more
standard functions. The generated implementation should end up the same,
since `Ordering.then` is `@[macro_inline]`.
2024-04-12 21:09:27 +00:00
.github chore: when setting up Mathlib CI, make sure nightly-with-mathlib branch has been fetched (#3834) 2024-04-05 00:40:50 +00:00
doc chore: update-stage0-commit cmake target (#3692) 2024-04-04 13:35:53 +00:00
images
nix chore: test results as job summary (#3715) 2024-03-27 10:14:33 +00:00
script fix: C++ exceptions across shared libraries on Linux (#3500) 2024-02-26 10:35:11 +00:00
src chore: use Ordering.then in deriving Ord (#3893) 2024-04-12 21:09:27 +00:00
stage0 fix: don't use info nodes before cursor for completion (#3778) 2024-04-02 08:49:24 +00:00
tests fix: omega: ignore levels in canonicalizer (#3853) 2024-04-10 08:46:07 +00:00
.gitattributes chore: Do not hide stage0/src/stdlib_flags.h from diffs 2023-09-13 19:29:25 +02:00
.gitignore chore: update tests to account for .lake 2023-11-13 20:31:24 -05: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
CODEOWNERS chore: update CODEOWNERS (#3878) 2024-04-11 04:21:42 +00:00
CONTRIBUTING.md doc: Adjust contributor's docs to squash merging (#2927) 2023-11-21 10:13:43 +00:00
flake.lock chore: test results as job summary (#3715) 2024-03-27 10:14:33 +00:00
flake.nix chore: replace shell.nix with a devShell in flake.nix (#3717) 2024-03-21 13:24:01 +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: remove nightly and other outdated references (#3027) 2024-01-25 13:53:36 +00:00
RELEASES.md feat: add pp.mvars and pp.mvars.withType (#3798) 2024-03-29 18:03:05 +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.