Leonardo de Moura
|
3cd81051c6
|
refactor(library/data/real/division): remove unnecessary 'xrewrite'
|
2015-06-27 14:07:32 -07:00 |
|
Jeremy Avigad
|
f8d8a2aed6
|
feat(library/data/nat/div): add characterization of mod
|
2015-06-27 18:51:44 +10:00 |
|
Jeremy Avigad
|
829c3fb22c
|
refactor(library/data/int/div): reorient of_nat_div and of_nat_mod
|
2015-06-27 18:47:36 +10:00 |
|
Jeremy Avigad
|
7c118f40fe
|
feat(library/data/nat/sub): add calculation facts for sub
|
2015-06-27 18:41:57 +10:00 |
|
Leonardo de Moura
|
a2cbf3dbca
|
refactor(library/data/fin): adjust proofs to support new approach for projections
|
2015-06-26 17:18:29 -07:00 |
|
Floris van Doorn
|
124c9d3d8a
|
feat(hott): various cleanup and fixes, rename \~ to ~, expand types.pointed
|
2015-06-25 22:31:40 -04:00 |
|
Leonardo de Moura
|
d2e64d30e8
|
refactor(library/data/quotient): make proofs more robust
|
2015-06-25 17:48:58 -07:00 |
|
Jeremy Avigad
|
a0461262d0
|
feat(library/data/real/*.lean): migrate theorems from algebra
|
2015-06-25 17:30:12 -07:00 |
|
Rob Lewis
|
4161b9ccbf
|
feat(library/data/real): rearrange constant sequence theorems to introduce rat coercion earlier. begin migrating theorems from algebra
|
2015-06-25 17:30:12 -07:00 |
|
Rob Lewis
|
afcf785f03
|
chore(library/data): update data.md
|
2015-06-25 17:30:12 -07:00 |
|
Leonardo de Moura
|
8967f57818
|
refactor(library/data/list): reduce reliance on definitional equality
|
2015-06-24 15:58:19 -07:00 |
|
Jeremy Avigad
|
7d204fdd91
|
refactor(library/data/finset/card.lean): add useful facts, shorter proof of eq_card_of_eq_subset
|
2015-06-20 21:13:00 -07:00 |
|
Leonardo de Moura
|
ee0d919c6f
|
feat(library/data/finset/card): add eq_of_card_eq_of_subset theorem
|
2015-06-19 20:05:32 -07:00 |
|
Leonardo de Moura
|
2910c780d0
|
feat(library/data/finset/basic): add auxiliary card lemma
|
2015-06-19 20:05:32 -07:00 |
|
Leonardo de Moura
|
4246a64913
|
feat(library/data/finset/basic): add more theorems for finset erase
|
2015-06-19 20:05:32 -07:00 |
|
Leonardo de Moura
|
70fc05294b
|
refactor(library/local_context): avoid hack in local_context
|
2015-06-18 15:41:00 -07:00 |
|
Leonardo de Moura
|
d12b5613c6
|
feat(library/data/set): show that (set A) is a comm_semiring
|
2015-06-17 09:53:50 -07:00 |
|
Haitao Zhang
|
1aff1f7cde
|
fix(library/data/fintype/function): make inj_of_nodup and nodup_of_inj more general
|
2015-06-16 19:17:53 -07:00 |
|
Haitao Zhang
|
8817042318
|
feat(library/data/fin) : establish add_comm_group on fin using madd
|
2015-06-16 16:38:47 -07:00 |
|
Leonardo de Moura
|
d43e0891ae
|
fix(library/init/logic): make sure library can be compiled using '--to_axiom' option
|
2015-06-16 13:10:08 -07:00 |
|
Rob Lewis
|
a72ca936c0
|
chore(library/real): replace theorems with versions from algebra
|
2015-06-16 11:30:12 -07:00 |
|
Rob Lewis
|
b94d0a948d
|
chore(library/data/real): replace theorems with more general versions from algebra
|
2015-06-16 11:30:12 -07:00 |
|
Rob Lewis
|
8d0518444d
|
chore(library/data/{pnat, real}): rename pnat theorems
|
2015-06-16 11:30:12 -07:00 |
|
Rob Lewis
|
ff0ba6687e
|
feat(library/algebra/ordered_field): move identity about abs to ordered_field
|
2015-06-16 11:30:12 -07:00 |
|
Rob Lewis
|
090f00458d
|
chore(library/data/real): remove redundant theorems
|
2015-06-16 11:30:12 -07:00 |
|
Rob Lewis
|
34868d196e
|
feat(library/data/rat): define pos natural upper bounds of rationals
|
2015-06-16 11:30:12 -07:00 |
|
Rob Lewis
|
1f4765e30a
|
feat(library/algebra/ordered_ring): add theorems used for rational upper bounds
|
2015-06-16 11:30:12 -07:00 |
|
Rob Lewis
|
cf7c85e5fd
|
feat(library/data/real): fill in lots of sorrys about pnats
|
2015-06-16 11:30:12 -07:00 |
|
Rob Lewis
|
a79ec6b0d4
|
feat(library/data/pnat): move facts about positive nats to their own file
|
2015-06-16 11:30:12 -07:00 |
|
Jeremy Avigad
|
9249ebdaab
|
feat(library/data/{nat,int}/div.lean): add properties of add and mod
|
2015-06-15 22:53:11 +10:00 |
|
Jeremy Avigad
|
a4a8253f50
|
refactor(library,hott,tests): rename succ_inj to succ.inj, add abbreviation eq_of_succ_eq_succ
|
2015-06-15 22:52:38 +10:00 |
|
Haitao Zhang
|
679bb8b862
|
feat(library/data/fin): add more theorems on finite ordinals
Add defintional equalities, properties of lifting and lowering functions, and definitions of madd.
|
2015-06-14 20:49:47 -07:00 |
|
Haitao Zhang
|
844d59c2ae
|
feat(library/data/fintype/function): add theorems of all nodup lists and all injective functions
|
2015-06-14 20:49:47 -07:00 |
|
Haitao Zhang
|
ef4b4d19ce
|
feat(library/data/list/basic): add cons related equalities
|
2015-06-14 16:59:56 -07:00 |
|
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 |
|
Haitao Zhang
|
1a9521dc9c
|
fix(library/data/fintype/function): convert line endings from crlf to lf
|
2015-06-11 15:29:43 -07:00 |
|
Leonardo de Moura
|
1b5d1136d9
|
refactor(library/data/finset/card): remove unnecessary xrewrite
We can use the default 'rewrite' tactic after the commits pushed today.
|
2015-06-10 18:46:16 -07:00 |
|
Leonardo de Moura
|
dc8768627c
|
refactor(library/data/fintype/function): cleanup proof
|
2015-06-10 18:21:15 -07:00 |
|
Leonardo de Moura
|
8fbe22f263
|
refactor(library/data/finset/basic): cleanup proof
|
2015-06-10 18:19:16 -07:00 |
|
Leonardo de Moura
|
226a5800dd
|
fix(library/data/rat/order): adjust file to recent changes
|
2015-06-10 16:56:17 -07:00 |
|
Jeremy Avigad
|
3c1f5f4e33
|
feat(library/data/{set,finset}): add more cardinality facts, rename, and add a lemma from Haitao
|
2015-06-10 16:39:17 -07:00 |
|
Jeremy Avigad
|
658c5a2c49
|
feat(library/rat/basic.lean): add reduce for rat, and num and denom
|
2015-06-10 16:39:17 -07:00 |
|
Leonardo de Moura
|
4b91cfccff
|
feat(frontends/lean/builtin_exprs): make notation ( e : T ) builtin
In the previous approach, the following (definitionally equal) term was being generated
(fun (A : Type) (a : A), a) T e
|
2015-06-10 14:52:59 -07:00 |
|
Rob Lewis
|
d287b20018
|
chore(library/data/real): move more lemmas to algebra
|
2015-06-09 16:27:55 +10:00 |
|
Rob Lewis
|
01f0bb827c
|
feat(library/data/real): use new algebra lemmas in completeness proof
|
2015-06-09 16:14:52 +10:00 |
|
Rob Lewis
|
b1aea149db
|
chore(library/data/real): update md
|
2015-06-09 15:43:43 +10:00 |
|
Rob Lewis
|
e112468f99
|
feat(library/data/real): prove reals are Cauchy complete
|
2015-06-09 15:39:51 +10:00 |
|
Rob Lewis
|
3749a8ad04
|
chore(library/data/real): update real.md
|
2015-06-09 15:39:51 +10:00 |
|
Leonardo de Moura
|
1c5c79fbc1
|
refactor(library/data/list/perm): use improved 'obtain' to cleanup proof
|
2015-06-08 11:58:21 -07:00 |
|