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 46b0fd35ec chore(util/numerics): remove Z/pZ field This abstraction was added when we started Lean. We wanted to focus on nonlinear arithmetic and support dReal. The zpz module was going to be used to implement polynomial factorization procedures similar to the ones in Z3 and computer algebra systems. This is not a goal for the Lean project anymore.		2018-04-12 16:43:10 -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	refactor(library/init/core,library/init/unit): make `unit` an abbreviation of `punit.{0}`	2018-03-27 10:33:04 -07:00
extras/latex	chore(extras/depgraph): remove leandeps	2017-07-15 02:27:17 -07:00
images	chore(CMakeLists.txt): move Lean logo to make sure we can test leanemacs without installing Lean	2015-01-31 17:38:49 -08:00
leanpkg	chore(leanpkg): delete	2018-04-10 12:43:17 -07:00
library	fix(init/core): typed_expr should accept Props	2018-04-12 16:14:47 +02:00
old_tests/tests	chore(*): disable test suite	2018-04-10 12:56:55 -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(script/deploy_nightly): show git log	2018-03-29 14:26:25 +02:00
src	chore(util/numerics): remove Z/pZ field	2018-04-12 16:43:10 -07:00
tests/lean	fix(init/core): typed_expr should accept Props	2018-04-12 16:14:47 +02: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	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	chore(.appveyor,.travis): disable leanpkg registry tests	2018-04-12 18:32:20 +02:00
LICENSE
README.md	chore(README): point CI links to lean4 branch	2018-04-12 13:50:42 +02:00