max/lean4-htt

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

Find a file

tydeu 3be4d74321 fix: lake: lowercase template exe name to avoid clash with lib		2023-09-14 02:15:37 -04:00
.github	chore: in nightly release notes, look for changes since last nightly	2023-09-01 11:08:18 +01:00
.vscode
doc	doc: update quickstart doc for release	2023-09-08 16:39:55 +02:00
images
nix	fix: If src is a dir, assume the lean file has the full path (#2465 )	2023-08-28 14:45:45 +02:00
script	fix: disabling forwarding --target to lean.	2023-08-14 13:33:46 +02:00
src	fix: lake: lowercase template exe name to avoid clash with lib	2023-09-14 02:15:37 -04:00
stage0	chore: update stage0	2023-09-13 17:45:54 +02:00
tests	feat: allow configuring occs in rw	2023-09-13 12:03:18 -07:00
.gitattributes	chore: Do not hide stage0/src/stdlib_flags.h from diffs	2023-09-13 19:29:25 +02:00
.gitignore	chore: .gitignore fixes	2023-08-02 04:03:56 -04:00
.ignore	chore: ignore stage0/ (for `rg` etc.)	2022-03-18 15:28:20 +01:00
CMakeLists.txt	feat: enable LLVM in stage1+ compiler	2023-08-14 13:33:46 +02:00
CONTRIBUTING.md	chore: update CONTRIBUTING.md	2023-02-01 12:07:15 -08:00
default.nix
flake.lock	chore: Nix bump to LLVM 15	2023-07-28 10:56:54 +02:00
flake.nix	chore: Nix: use strings instead of URL literals (#2172 )	2023-03-28 10:10:24 +02:00
LICENSE
LICENSES
README.md	chore: update README to reflect beginning stable releases (#2477 )	2023-08-29 13:24:19 +00:00
RELEASES.md	doc: update RELEASES.md for rename of `getConst?` (#2482 )	2023-08-30 04:44:23 +00:00
shell.nix	chore: Nix bump to LLVM 15	2023-07-28 10:56:54 +02:00

This is the repository for Lean 4.

We provide nightly releases and have just begun regular stable point releases.

About

Installation