michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
lean2/library/data
History
Leonardo de Moura b7023ce1d8 fix(frontends/lean/placeholder_elaborator): do not truncate stream of 
solutions during class-instance resolution, closes #183

For example, in theorem inverse_unique at category.lean, implicit
arguments are synthesized for inverse_compose. The first solution H' is
not good, and produces a type incorrect solution
2014-09-12 16:12:23 -07:00
..
int refactor(library): replace decidable_eq with abbreviation 2014-09-09 16:09:05 -07:00
list refactor(library/data/list/basic): cleanup 2014-09-10 16:42:49 -07:00
nat refactor(library): replace decidable_eq with abbreviation 2014-09-09 16:09:05 -07:00
quotient chore(library/data/quotient): rename aux.lean to util.lean (fix problem with cloning lean repository on Windows machine) 2014-09-11 14:57:15 -07:00
bool.lean refactor(library): replace decidable_eq with abbreviation 2014-09-09 16:09:05 -07:00
category.lean fix(frontends/lean/placeholder_elaborator): do not truncate stream of 2014-09-12 16:12:23 -07:00
data.md refactor(library): remove unnecessary 'standard' subdirectory 2014-08-23 18:08:09 -07:00
default.lean refactor(library): remove unnecessary 'standard' subdirectory 2014-08-23 18:08:09 -07:00
empty.lean feat(library/data/empty): add false.to_empty and false.rec_type theorems 2014-09-05 09:31:27 -07:00
num.lean refactor(library/data): cleanup datatypes 2014-09-04 22:31:52 -07:00
option.lean refactor(library): replace decidable_eq with abbreviation 2014-09-09 16:09:05 -07:00
prod.lean refactor(library): replace decidable_eq with abbreviation 2014-09-09 16:09:05 -07:00
set.lean refactor(library): add namespaces 'or', 'and' and 'iff' 2014-09-04 21:25:21 -07:00
sigma.lean fix(frontends/lean): name clash inside section, fixes #181 2014-09-11 16:37:23 -07:00
string.lean refactor(library/data): cleanup datatypes 2014-09-04 22:31:52 -07:00
subtype.lean refactor(library): replace decidable_eq with abbreviation 2014-09-09 16:09:05 -07:00
sum.lean refactor(library): replace decidable_eq with abbreviation 2014-09-09 16:09:05 -07:00
unit.lean refactor(library): replace decidable_eq with abbreviation 2014-09-09 16:09:05 -07:00
vector.lean feat(library/data/vector): add vec.is_inhabited theorem 2014-09-07 19:08:31 -07:00