max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/library/init/data
History
Leonardo de Moura 0c6108ce7a chore(library/init/data/quot): use Sort instead of Type 
Remark: The kernel was already using Sort. So, the limitation was
artificial. Moreover, it may seem unnecessary to have quotients of
proofs in a proof irrelevant system, but this is useful for proving
a more general funext lemma. This more general version is needed in
the new tested contributed by @digama0.
2017-03-07 14:29:57 -08:00
..
bool chore(library/init/data/bool/lemmas): add (coe tt) and (coe ff) simp lemmas 2017-03-05 09:50:01 -08:00
char feat(library/init/meta): use cheap "reflexivity" after simp and rewrite 2016-12-08 14:41:26 -08:00
fin feat(library/init/data/fin/ops): add def lemmas 2017-03-05 16:57:36 -08:00
int feat(library): add check_constants.lean validation, cleanup unused names, minor stdlib fixes 2017-02-21 10:45:31 -08:00
list chore(library/init/data/list/lemmas): remove old comment 2017-03-04 16:31:31 -08:00
nat feat(library/init/data/fin): add div 2017-03-05 16:43:15 -08:00
num
option chore(library/init/data/option/basic): add lift for option_t 2017-03-05 08:17:55 -08:00
sigma chore(library/init/data/quot): use Sort instead of Type 2017-03-07 14:29:57 -08:00
string feat(init/data/string/basic.lean): inhabited string 2016-12-23 14:45:53 -08:00
subtype feat(frontends/lean): no global universes in the frontend 2017-02-08 17:23:04 -08:00
sum feat(frontends/lean): no global universes in the frontend 2017-02-08 17:23:04 -08:00
unsigned feat(library/init/data/fin): add div 2017-03-05 16:43:15 -08:00
array.lean feat(library/init/data/array): add helper functions and instances 2017-02-21 13:45:03 -08:00
basic.lean feat(library/init/data/unsigned): add basic unsigned operations 2017-03-05 16:14:16 -08:00
default.lean feat(library/init/data/unsigned): add basic unsigned operations 2017-03-05 16:14:16 -08:00
ordering.lean
prod.lean feat(frontends/lean): no global universes in the frontend 2017-02-08 17:23:04 -08:00
quot.lean chore(library/init/data/quot): use Sort instead of Type 2017-03-07 14:29:57 -08:00
set.lean feat(frontends/lean): no global universes in the frontend 2017-02-08 17:23:04 -08:00
setoid.lean chore(library/init/data/quot): use Sort instead of Type 2017-03-07 14:29:57 -08:00
to_string.lean chore(library/init): instances are reducible and are inlined by the compiler 2017-03-07 10:58:09 -08:00
unit.lean refactor(library/data): delete init/data/instances.lean 2016-12-02 16:41:16 -08:00