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 19ee270c60 refactor(library): remove vector and bitvec from init Reason: vector in in init folder was introducing an overload (`::`) for all Lean users. The workaround (use `local infix ::`) was counterintuitive. We currently have no special support for bitvectors in the code generator. Thus, there is no need to have vector and bitvec in the init folder right now. Moreover, the new parser and elaborator (issue #1674) should provide better ways of managing overloaded symbols.		2017-08-16 13:40:50 -07:00
.github	chore(.github/ISSUE_TEMPLATE): typo	2017-07-14 08:02:08 +01:00
bin	dist: add leanpkg.bat script for invocation on Windows	2017-07-20 21:50:23 +01:00
doc	chore(init/algebra/order): typo	2017-08-02 15:41:51 +01:00
extras/latex	chore(extras/depgraph): remove leandeps	2017-07-15 02:27:17 -07:00
images
leanpkg	feat(leanpkg): make `test` imply `build`	2017-07-27 10:15:42 +02:00
library	refactor(library): remove vector and bitvec from init	2017-08-16 13:40:50 -07:00
script	chore(script/deploy_gh_pages): --reset-author	2017-07-27 10:23:16 +02:00
src	chore(init/meta/interactive): check simp lemmas for ambiguous overloads	2017-08-15 12:43:02 +02:00
tests	refactor(library): remove vector and bitvec from init	2017-08-16 13:40:50 -07:00
tmp	feat(frontends/lean,library/equations_compiler): store tactics for generating well founded relation and decreasing proofs	2017-05-23 15:00:29 -07:00
.appveyor.yml	chore(.appveyor.yml,.travis.yml): simplify using glob patterns	2017-07-26 17:13:34 +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
.gitignore	chore(gitignore): ignore nix files	2017-06-19 13:16:04 +02:00
.travis.yml	chore(.appveyor.yml,.travis.yml): simplify using glob patterns	2017-07-26 17:13:34 +02:00
LICENSE
README.md	feat(doc/export_format): advertise trepplein	2017-07-15 22:49:24 +01:00