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 182812a278 chore(library/init/lean/parser/token): make sure generate code does contain partially applied `reader_t.or_else` and `reader_t.bind` @kha This one was crazy, the compiler created a join point for the continuation of the match-expression. Each case of the match was invoking the join point with a different parser. Two of the branches were the partially applied `reader_t.bind` and `reader_t.orelse`. This change did not improve the performance much, but it makes sure we don't waste time trying to figure out why we have these two partial applications in the call graph.		2018-11-08 17:39:46 -08:00
.github	chore(.github/CONTRIBUTING): fix typos and URLs	2017-10-30 16:23:22 +01:00
bin	chore(bin/lean-gdb): exclude scalar fields	2018-10-04 18:32:03 -07:00
doc	doc(doc/coding_style,doc/commit_convention): fix git hook commands	2018-07-05 10:20:25 +02:00
gen	fix(runtime/apply): must use `free_heap_obj` instead of `free`	2018-08-28 12:29:14 -07:00
images
lean4-mode	feat(lean4-mode/lean4-flycheck): store .olean of dependencies	2018-09-11 16:35:25 -07:00
library	chore(library/init/lean/parser/token): make sure generate code does contain partially applied `reader_t.or_else` and `reader_t.bind`	2018-11-08 17:39:46 -08:00
script	chore(script/lib_perf): adapt to change in `lean` command line behavior	2018-09-27 13:11:42 -07:00
src	perf(library/compiler/csimp): avoid unnecessary local decl	2018-11-08 17:03:34 -08:00
tests	perf(library/init/lean/parser): move backtrackable state from parser_core_t to module_parser_m	2018-11-08 15:58:41 +01: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 library/Makefile	2018-11-07 09:30:32 +01: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