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 77ae133baa fix(library/type_context): preprocess_class @kha This commit fixes the bug we discussed on slack. I had to repair one of the tests. The broken test made me realize that if we use the unbundled approach to define something like `is_semiring` ``` class is_semiring (α : Type) (plus : α → α → α) (mul : α → α → α) (zero : out_param α) (one : out_param α) := ... ``` Then, to retrieve a `is_semiring` instance, we need to know `α`, `plus` and `mul`. This is problematic because we may be in a context where one of them cannot be inferred. This would force user to manually provide the missing (input) parameter. We are not considering the unbundled approach for complex algebraic structures such as `semiring`, `ring` and `field`, but I wanted to document this limitation here since we may face it in other type classes. I think it is a bad idea to add back `inout_param` and have both: `inout_param` and `out_param`. The previous `inout_param` created many instabilities and hard to diagnose failures.		2018-01-24 17:30:04 -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	refactor(library/io): make `io` easier to extend and use	2018-01-23 15:03:31 -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	chore(library/system/io): `tactic.run_io` ==> `tactic.unsafe_run_io`	2018-01-24 10:32:32 -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/test_registry): Replace with leanpkg. Execute in every artifact-producing build configuration.	2017-12-20 14:01:45 -08:00
src	fix(library/type_context): preprocess_class	2018-01-24 17:30:04 -08:00
tests	fix(library/type_context): preprocess_class	2018-01-24 17:30:04 -08:00
tmp	feat(library/init/data): start rbtree module	2017-11-15 16:17:39 -08:00
.appveyor.yml	chore(script/test_registry): Replace with leanpkg. Execute in every artifact-producing build configuration.	2017-12-20 14:01:45 -08: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	fix(build): fix Cygwin build	2018-01-22 18:07:04 -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(doc/make): add platform-generic build instructions	2018-01-23 11:14:18 -08:00