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 5428767f11 refactor(library/tactic): remove two thread local caches The AC manager cache will be rewritten for the AC matcher. The congruence closure module has to be rewritten for performance reasons. During the rewrite, we should evaluate whether we need a new cache management policy or not.		2018-02-21 15:04:19 -08: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	feat(library/time_task): print cumulative times on --profile	2018-02-19 09:13:24 -08:00
extras/latex	chore(extras/depgraph): remove leandeps	2017-07-15 02:27:17 -07:00
images
leanpkg	refactor(library/io): make `io` easier to extend and use	2018-01-23 15:03:31 -08:00
library	feat(library/init/data/nat/lemmas): add lemma for termination proofs	2018-02-21 10:37:07 -08: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(script/lib_perf): make interruptible and fix uninitialized variable	2018-02-19 09:13:24 -08:00
src	refactor(library/tactic): remove two thread local caches	2018-02-21 15:04:19 -08:00
tests	feat(kernel/inductive): make sure constructor types do not contain local constants nor metavariables	2018-02-21 15:04:19 -08:00
tmp	doc(tmp/fresh_name): document impact of new `mk_fresh_name` design on thread local caches	2018-02-01 18:06:19 -08:00
.appveyor.yml	chore(.appveyor.yml): fix core update	2018-02-17 22:18:02 +01:00
.clang-format	feat(library/vm/process): add basic process support	2017-03-28 18:08:06 -07:00
.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	doc(msvc): add instructions on how to get Intellisense working	2018-02-06 10:11:10 -08:00
.travis.yml	fix(.travis.yml): support combining $TEST_LEANPKG_REGISTRY and $UPLOAD	2017-12-22 11:54:29 +01:00
LICENSE
README.md	chore(README.md) fixing link to download page	2018-02-15 11:36:12 +01:00