Haitao Zhang
|
798b240149
|
fix(library/data/list/comb): adjust dmap related names to comply with convention
|
2015-06-14 16:59:56 -07:00 |
|
Haitao Zhang
|
6105263222
|
feat(library/data/list/comb): add theorem on dmap and adjust names
|
2015-06-11 15:29:52 -07:00 |
|
Jeremy Avigad
|
f475408f4c
|
feat(library/data/list/*): add theorems from Haitao Zhang and clean up
|
2015-06-05 09:32:00 -07:00 |
|
Floris van Doorn
|
7f5caab694
|
feat(nat): redefine le and lt in the standard library
|
2015-06-04 20:14:13 -04:00 |
|
Leonardo de Moura
|
63f61a35f4
|
feat(library/data/list/set): cleanup nodup_map proof
|
2015-06-04 15:21:40 -07:00 |
|
Jeremy Avigad
|
df69bb4cfc
|
feat(library/*): add theorems from Haitao on sets and functions, clean up
|
2015-06-04 11:55:25 -07:00 |
|
Leonardo de Moura
|
19361f0196
|
feat(library/unifier): do not fire type class resolution as last resort when type contains metavariables
see discussion at #604
|
2015-05-18 15:45:23 -07:00 |
|
Jeremy Avigad
|
6fce01385c
|
feat(library/data/{finset,list}/bigop.lean: generalize bigops from group to monoid
|
2015-05-08 19:51:37 +10:00 |
|
Jeremy Avigad
|
42f2fc973a
|
refactor(library/data/{finset,list,fintype}: rename cross_product to product
|
2015-05-08 19:51:37 +10:00 |
|
Jeremy Avigad
|
86a039b6d5
|
feat(library/data/list/set.lean): add two theorems
|
2015-05-08 19:51:37 +10:00 |
|
Leonardo de Moura
|
11f74363e2
|
refactor(library): rename 'intersection' to 'inter' in list and finset, add finset abbreviation at top level
|
2015-05-05 08:53:31 -07:00 |
|
Leonardo de Moura
|
3b84a63874
|
fix(library/algebra/function): terminology
|
2015-04-16 20:52:18 -07:00 |
|
Leonardo de Moura
|
f523d3a995
|
feat(library/data): add structure for converting a list of elements into a type, and then show the resultant type is a finite type
|
2015-04-12 17:33:58 -07:00 |
|
Leonardo de Moura
|
41ddc97e0d
|
feat(library/data/list): define filter function for lists
|
2015-04-11 18:22:22 -07:00 |
|
Leonardo de Moura
|
06d4ae971d
|
feat(library/data/list): add nodup_cross_product theorem
|
2015-04-11 14:31:01 -07:00 |
|
Leonardo de Moura
|
54a2d9750e
|
refactor(library/data): simplify definition of disjoint
|
2015-04-11 14:04:09 -07:00 |
|
Leonardo de Moura
|
1b34f40f36
|
feat(library/data/list/set): add decidable_nodup
|
2015-04-11 09:39:26 -07:00 |
|
Leonardo de Moura
|
5304c5afb8
|
feat(library/data/list/set): add 'all' theorems
|
2015-04-11 09:28:05 -07:00 |
|
Leonardo de Moura
|
a24c0bf1db
|
feat(library/data/finset): define intersection for finsets
|
2015-04-10 16:45:25 -07:00 |
|
Leonardo de Moura
|
49d6d43926
|
feat(library/data/list): define intersection for lists
|
2015-04-10 16:31:44 -07:00 |
|
Leonardo de Moura
|
d59c671054
|
feat(library/data/list/comb): define upto list generator
|
2015-04-10 15:32:44 -07:00 |
|
Leonardo de Moura
|
4be8741a39
|
feat(library/data/list): break list/basic.lean into smaller files
|
2015-04-10 05:19:52 -07:00 |
|