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 ac0352b584 refactor(kernel): remove quotitent normalizer extension The `quot` type is now implemented in the kernel. We will do the same thing for inductives. We will not support normalizer extensions anymore in Lean4. It doesn't make sense since we settled with 2 extensions: quotients and inductives. Moreover, any new extension would require substantial changes (e.g., code generator). The normalizer_extension feature was useful when we were experimenting with different kernel flavors.		2018-06-01 10:52:17 -07:00
.github	chore(.github/CONTRIBUTING): fix typos and URLs	2017-10-30 16:23:22 +01:00
bin	chore(bin/lean-gdb): add pretty printer for lean::level	2017-11-30 17:47:49 +01:00
doc	doc(doc/make/emscripten): document Emscripten build	2018-04-30 18:17:16 +02:00
extras/latex	chore(extras/depgraph): remove leandeps	2017-07-15 02:27:17 -07:00
gen	chore(runtime): `lean_obj.` ==> `object.`	2018-05-20 10:17:15 -07:00
images
leanpkg	chore(leanpkg): delete	2018-04-10 12:43:17 -07:00
library	refactor(kernel): remove quotitent normalizer extension	2018-06-01 10:52:17 -07:00
old_tests/tests	feat(frontends/lean/definition_cmds): elaborate a def's type separately when explicit return type is given	2018-04-20 09:59:09 -07:00
packages	chore(script/test_registry): Replace with leanpkg. Execute in every artifact-producing build configuration.	2017-12-20 14:01:45 -08:00
script	chore(*): fix tests	2018-05-21 06:57:43 -07:00
src	refactor(kernel): remove quotitent normalizer extension	2018-06-01 10:52:17 -07:00
tests	test(tests/lean/smart_unfolding): add smart_unfolding test back	2018-06-01 09:07:04 -07:00
tmp	chore(tmp/lean4.md): moved to google docs	2018-03-20 17:26:43 -07:00
.appveyor.yml	chore(.appveyor,.travis): disable leanpkg registry tests	2018-04-12 18:32:20 +02:00
.clang-format
.codecov.yml	fix(.codecov.yml): do not fail github ci if coverage drops by 0.01%	2017-06-25 10:35:02 +02:00
.gitattributes	chore(.gitattributes): use `union` merge strategy for doc/changes.md	2017-12-11 12:49:10 +01:00
.gitignore	chore(.gitignore): ignore `*.produced.out` files	2018-05-01 08:43:46 -07:00
.travis.yml	chore(.travis.yml): trigger AppVeyor nightly build from Travis	2018-04-13 16:44:27 +02:00
LICENSE
README.md	chore(README): point CI links to lean4 branch	2018-04-12 13:50:42 +02:00