lean4-htt

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

Find a file

Leonardo de Moura a535d348de feat(library/init/lean/elaborator): use `SyntaxNode` to define `TermElab` and `CommandElab`		2019-07-21 07:29:41 -07:00
.github
bin	chore(bin/leanc): set increased stack size on Windows	2019-07-05 11:24:15 +02:00
doc	doc(doc/make/msys2): update instructions	2019-07-05 11:24:15 +02:00
images
lean4-mode	feat(library/init): use new "empty match" syntax	2019-07-15 16:25:14 -07:00
library	feat(library/init/lean/elaborator): use `SyntaxNode` to define `TermElab` and `CommandElab`	2019-07-21 07:29:41 -07:00
script	chore(script/prepare-commit-msg): fix suffix pattern	2019-07-05 16:22:06 +02:00
src	chore(runtime,library/init/lean): remove evalConst	2019-07-19 11:04:57 -07:00
tests	chore(tests/bench): fix syntax	2019-07-19 10:46:02 +02:00
tmp/new-frontend	chore(library/init/lean): disable new frontend for now	2019-06-05 15:26:43 -07:00
.appveyor.yml
.clang-format
.codecov.yml
.gitattributes
.gitignore	feat(default.nix,tests/playground): Nix-powered benchmark suite	2019-05-15 13:25:29 +02:00
.travis.yml
azure-pipelines.yml	chore(azure-pipelines.yml): Azure Pipelines CI	2019-07-05 11:24:15 +02:00
default.nix	chore(default.nix): factor out derivation	2019-07-05 11:24:15 +02:00
derivation.nix	chore(default.nix): factor out derivation	2019-07-05 11:24:15 +02:00
LICENSE
README.md	chore(README): update	2019-04-24 11:40:46 -07:00
shell.nix	chore(shell.nix): update temci once more	2019-07-04 16:59:57 +02:00

We are currently developing Lean 4. Lean 3 is still the latest official release. This repository contains work in progress.

Important. Unless you are one of our collaborators