lean4-htt

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

Find a file

Sebastian Ullrich 9527058df9 feat: Nix: support overriding stage 0 for chaining builds with different configurations/source trees		2020-11-29 18:59:39 +01:00
.github	fix: Nix: don't try to push PRs	2020-11-24 19:16:27 +01:00
doc	doc: add `typeclass.md`	2020-11-26 08:42:42 -08:00
images
lean4-mode	feat: nicer syntax for unification hints	2020-11-27 19:18:18 -08:00
nix	feat: Nix: support overriding stage 0 for chaining builds with different configurations/source trees	2020-11-29 18:59:39 +01:00
script	chore: delete obsolete scripts	2020-10-14 19:14:00 +02:00
src	chore: helper trace message	2020-11-29 08:46:34 -08:00
stage0	chore: update stage0	2020-11-29 08:05:27 -08:00
tests	test: add coercion pullback example from "Hints in Unification"	2020-11-29 08:46:45 -08:00
tmp	chore: remove tactic framework dependency	2020-11-10 14:32:58 -08:00
.gitattributes	chore: restore marking stage0/ as binary files, which we lost at some point	2020-08-14 11:12:13 +02:00
.gitignore	chore: ignore `result` files from nix build	2020-11-24 19:16:27 +01:00
CMakeLists.txt	chore: use standard release build for stage 0	2020-10-12 10:34:48 +02:00
default.nix	feat: Nix: compatibility default.nix	2020-11-24 19:16:27 +01:00
flake.lock	feat: Nix: mdbook	2020-11-24 19:16:27 +01:00
flake.nix	feat: Nix: sanitized build	2020-11-29 14:08:53 +01:00
LICENSE
README.md	chore: add link to manual	2020-11-23 10:21:52 -08:00
shell.nix	fix: CI: Linux release job	2020-11-24 19:16:27 +01:00

We are currently developing Lean 4. The Lean 4 manual (work in progress) will give you an overview of the language.

Lean 3 is still the latest official release. This repository contains work in progress.

Important. Unless you are one of our collaborators