Leonardo de Moura
|
41ddc97e0d
|
feat(library/data/list): define filter function for lists
|
2015-04-11 18:22:22 -07:00 |
|
Leonardo de Moura
|
c437fbe0bc
|
feat(library/data/fintype): prove that A->B has decidable equality when A is a finite type and B has decidable equality
|
2015-04-11 16:45:27 -07:00 |
|
Leonardo de Moura
|
3df7fe120c
|
feat(library/algebra/function): define curry and uncurry functions
|
2015-04-11 16:45:07 -07:00 |
|
Leonardo de Moura
|
3edf0dffdf
|
feat(library/data/finset): define subset for finsets
|
2015-04-11 15:29:12 -07:00 |
|
Leonardo de Moura
|
dfef4c5daf
|
feat(library/data): define fintype type class
|
2015-04-11 14:55:41 -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
|
ee895e00dd
|
feat(library/data/list): define cross_product for lists
|
2015-04-11 13:52:50 -07:00 |
|
Leonardo de Moura
|
fefddcd0f9
|
fix(library/data/list/perm): broken theorem
|
2015-04-11 09:42:24 -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
|
dff05557a3
|
feat(library/data/finset): add all combinator theorems
|
2015-04-11 09:28:27 -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
|
32b07c4561
|
feat(library/data/finset): define map for finset
|
2015-04-10 17:14:10 -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
|
9d8b5aa347
|
feat(library/data/list/comb): add any/all theorems
|
2015-04-10 07:01:14 -07:00 |
|
Floris van Doorn
|
60ae9f627c
|
feat(hott): add core.hlean and types/default.hlean
|
2015-04-10 06:35:24 -07:00 |
|
Floris van Doorn
|
d1b98b6919
|
fix(reserved_notation): make is_typeof an abbreviation
|
2015-04-10 06:35:15 -07:00 |
|
Leonardo de Moura
|
5caa983919
|
feat(library/data/finset): redefine bigop for finset
|
2015-04-10 06:13:32 -07:00 |
|
Leonardo de Moura
|
53f730ec82
|
feat(library/data/list/bigop): add bigop perm theorem
|
2015-04-10 06:01:23 -07:00 |
|
Leonardo de Moura
|
608e2838bf
|
feat(library/data/list): define bigop for lists
|
2015-04-10 05:52:19 -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 |
|
Leonardo de Moura
|
a223b9b1f7
|
feat(library/data/finset): add bigop for finset + commutative groups
|
2015-04-09 20:00:00 -07:00 |
|
Leonardo de Moura
|
795acc70a6
|
refactor(library/data/finset): move finset to its own directory
|
2015-04-09 19:30:09 -07:00 |
|
Leonardo de Moura
|
ca377e5f8b
|
feat(library/data/list/basic): add foldr/foldl theorems
|
2015-04-09 18:48:04 -07:00 |
|
Leonardo de Moura
|
b209f442f7
|
refactor(library/data/list) fix theorem name, and do not rely on implementation of mem
|
2015-04-09 16:27:48 -07:00 |
|
Leonardo de Moura
|
4416d9b2c5
|
test(tests/lean/run): add basic tests for finset module
|
2015-04-09 15:56:41 -07:00 |
|
Leonardo de Moura
|
2ab2f7dc9d
|
feat(library/data/finset): add basic support for finite sets
|
2015-04-09 15:51:23 -07:00 |
|
Leonardo de Moura
|
571ff76080
|
feat(library/data/list/perm): add perm_ext theorem
|
2015-04-09 15:27:32 -07:00 |
|
Leonardo de Moura
|
64173ddf93
|
feat(library/data/list/basic): more nodup theorems
|
2015-04-09 14:50:00 -07:00 |
|
Leonardo de Moura
|
b4611ba33d
|
feat(library/data/list/basic): add mem erase theorems
|
2015-04-09 13:19:51 -07:00 |
|
Leonardo de Moura
|
5ba5e66665
|
feat(library/algebra/binary): add auxiliary theorems
|
2015-04-09 11:00:59 -07:00 |
|
Leonardo de Moura
|
d5176ebae5
|
refactor(library/algebra/binary): define right_commutative and left_commutative
|
2015-04-09 10:54:28 -07:00 |
|
Leonardo de Moura
|
8522fbec4b
|
feat(library/data/list): more general theorems for perm foldl and foldr, and other minor improvements
|
2015-04-09 09:29:58 -07:00 |
|
Leonardo de Moura
|
07ff0900aa
|
feat(library/data/list): add permutation theorems for union and insert
|
2015-04-08 19:02:35 -07:00 |
|
Leonardo de Moura
|
33422a387a
|
feat(library/data/list/basic): define 'union' and 'insert' for lists
|
2015-04-08 18:12:51 -07:00 |
|
Leonardo de Moura
|
c95bd8ba61
|
feat(library/data/list): add erase_dup and theorems
|
2015-04-08 12:28:48 -07:00 |
|
Leonardo de Moura
|
05bd6b5fe7
|
feat(library/data/list): add foldr/foldl equality theorems for permutations
|
2015-04-08 10:36:05 -07:00 |
|
Leonardo de Moura
|
24f1454c0a
|
fix(tests/lean/interactive/findp): adjust test output to reflect recent changes in the pretty printer
|
2015-04-08 09:49:22 -07:00 |
|
Jeremy Avigad
|
eb5089bf27
|
feat(library/data/set): add theory of functions and maps between sets
|
2015-04-08 09:46:34 -07:00 |
|
Jeremy Avigad
|
1f4ddd7a0f
|
refactor(library/init/funext.lean): break out definition of equivalence, and hide auxiliary theorems
|
2015-04-08 09:46:34 -07:00 |
|
Jeremy Avigad
|
5812b35d93
|
feat(library/data/set/function.lean): begin theory of functions on sets
|
2015-04-08 09:46:34 -07:00 |
|
Leonardo de Moura
|
afc75f141c
|
refactor(library/data/list/perm): prove auxiliary theorems using 'match-with'
|
2015-04-08 09:43:17 -07:00 |
|
Leonardo de Moura
|
56d20852aa
|
refactor(library/data/list/perm): remove dead code
|
2015-04-08 09:32:28 -07:00 |
|
Leonardo de Moura
|
ef1b057b63
|
refactor(library/data/list/perm): cleanup theorem
|
2015-04-08 09:29:40 -07:00 |
|
Leonardo de Moura
|
e0e65705db
|
feat(library/data/list/perm): add perm inversion theorems
|
2015-04-07 18:54:02 -07:00 |
|
Leonardo de Moura
|
c6a35e718d
|
refactor(library/data/list/perm): use by_cases instead of dependent-if
|
2015-04-07 09:26:24 -07:00 |
|
Leonardo de Moura
|
9306830d8c
|
feat(library/data/list): perm is decidable
|
2015-04-07 09:12:10 -07:00 |
|
Leonardo de Moura
|
1d87016f03
|
refactor(library): move some theorems to init
|
2015-04-07 07:46:11 -07:00 |
|