lean4-htt

Lean 4 fork for HoTT-compatible kernel extensions (Path types, transport, HITs). Maintained against upstream leanprover/lean4.

Find a file

Gabriel Ebner 54114fd7bd fix(frontends/lean/tactic_notation): do not clamp errors to the end of {} blocks		2017-05-23 07:28:34 +02:00
bin	chore(bin/lean-gdb): pretty-print lean::optional	2017-05-09 16:02:41 -07:00
doc
extras
images
leanpkg
library	fix(frontends/lean/tactic_notation): do not clamp errors to the end of {} blocks	2017-05-23 07:28:34 +02:00
old_library
script
src	fix(frontends/lean/tactic_notation): do not clamp errors to the end of {} blocks	2017-05-23 07:28:34 +02:00
tests	fix(frontends/lean/tactic_notation): do not clamp errors to the end of {} blocks	2017-05-23 07:28:34 +02:00
tmp	feat(frontends/lean/definition_cmds): copy equational lemmas to top level definition	2017-05-22 14:51:06 -07:00
.appveyor.yml
.appveyor.yml.in
.clang-format
.codecov.yml
.gitignore
.travis.yml
.travis.yml.in
LICENSE
README.md

License	Windows	Linux / macOS	Test Coverage	Chat

About