Rob Lewis
|
82950e1c52
|
chore(library/algebra/ordered_field): remove redundant line in calc
|
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 |
|
Leonardo de Moura
|
018518f0cf
|
refactor(library/algebra/ring): more robust proofs
|
2015-06-22 15:31:03 -07:00 |
|
Leonardo de Moura
|
7ffabeb245
|
refactor(library/algebra/group): avoid abuse of rewrite tactic
The two instances are relying on the fact that (a - b) reduces to (a + -b)
|
2015-06-22 15:11:14 -07:00 |
|
Leonardo de Moura
|
cfafc90cc0
|
refactor(hott,library): make sure files compile even without using "projection macros"
|
2015-06-22 12:22:11 -07:00 |
|
Jeremy Avigad
|
d28eb919f1
|
refactor(library/logic/axioms/examples/diaconescu.lean): mild reformatting, to match tutorial
|
2015-06-20 21:13:00 -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
|
5f293cee9c
|
refactor(library/algebra/ordered_field): improve compilation time
|
2015-06-18 16:12:24 -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
|
a4c0699e81
|
feat(library/tactic/constructor_tactic): restore 'constructor' tactic old semantics, add 'fconstructor' tactic
See issue #676
Add new test demonstrating why it is useful to have the old semantics
for 'constructor'
|
2015-06-17 23:48:54 -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 |
|
Leonardo de Moura
|
b80a391d63
|
fix(library/init/sigma): make sure file compiles even when '--to_axiom' is used
|
2015-06-16 12:52: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
|
f7ab2780d4
|
feat(library/algebra): move more theorems from reals to 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
|
b23e23061f
|
feat(library/algebra): finish/move more general theorems from reals to 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
|
4b38e14586
|
feat(library/algebra/ordered_field): add a couple missing theorems to ordered_field
|
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
|
6b36076ab5
|
feat({library,hott}/init/nat): add sub_le_succ
|
2015-06-15 22:53:11 +10:00 |
|
Jeremy Avigad
|
3b010b8c92
|
feat({library,hott}/algebra/group): add abbreviations e.g. for mul.cancel_left
|
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 |
|
Leonardo de Moura
|
ff5022c2f4
|
feat(library/data/axioms): add 'type_decidable'
In Lean standard mode, Hilbert choice implies that all types are
decidable.
|
2015-06-14 17:33:22 -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 |
|
Leonardo de Moura
|
1bffb89126
|
fix(library/algebra/function): lean was failing to infer that injective is a decidable predicate for finite types with decidable equality
This is an issue reported by Haitao.
|
2015-06-09 15:30:58 -07:00 |
|