Leonardo de Moura
|
89f69630b6
|
feat(library): use sigma instead of exists (experimental)
|
2015-07-15 15:49:47 -04:00 |
|
Haitao Zhang
|
5034de9c4e
|
feat(library/data/nat/power): add nat power divide theorems
|
2015-07-13 22:02:17 -04:00 |
|
Jeremy Avigad
|
31aeff95d5
|
refactor(library/algebra/ordered_ring): remove 0 ~= 1 from ordered_semiring, add 0 < 1 to linear_ordered_semiring
|
2015-07-07 21:05:48 -07:00 |
|
Jeremy Avigad
|
e35f05ad47
|
feat(library/data/nat/order): add greatest i < n st P i
|
2015-07-07 21:05:48 -07:00 |
|
Jeremy Avigad
|
b19331f28f
|
feat(library/data/nat/order): add theorems for max and min
|
2015-06-29 15:23:11 +10:00 |
|
Jeremy Avigad
|
70e551c6d6
|
feat(library/algebra/order,library/data/nat/order,library/*): instantiate nat to lattice, add theorems
|
2015-06-29 15:23:11 +10:00 |
|
Floris van Doorn
|
ff41886a32
|
feat(nat/bquant): give instances for quantification bounded with le
also add theorems c_iff_c to logic/connectives, where c is a connective
|
2015-06-04 20:14:13 -04: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
|
7a39d5aaa3
|
feat(library/data): add auxiliary definitions
|
2015-06-02 22:08:25 -07:00 |
|
Jeremy Avigad
|
b76445df39
|
feat(library/data/{nat,int}/div.lean,*): improve and extend div in nat and int
|
2015-05-30 22:10:21 +10:00 |
|
Rob Lewis
|
6dfcc4610b
|
feat(data): update orderings on int and nat to conform to new algebraic hierarchy
|
2015-05-29 14:11:51 +10:00 |
|
Leonardo de Moura
|
dc6411b903
|
feat(library/inductive_unifier_plugin): restrict rule that was generating non-terminating behavior
see issue #632
|
2015-05-27 14:41:12 -07:00 |
|
Leonardo de Moura
|
4152ebfa23
|
refactor(library/data/nat): use new tactics
|
2015-05-25 18:14:52 -07:00 |
|
Jeremy Avigad
|
39129f112b
|
refactor(library/*): do various renamings
|
2015-05-25 16:50:42 -07:00 |
|
Jeremy Avigad
|
fdc89cd285
|
refactor(library/algebra/order.lean,library/{data,algebra}/*): use better names for order theorems
|
2015-05-25 16:50:42 -07:00 |
|
Jeremy Avigad
|
81c0ef8c89
|
refactor(library/data/nat/*): cleanup, additions, renaming
|
2015-05-25 16:50:42 -07:00 |
|
Jeremy Avigad
|
f65a49b2c3
|
feat/fix(library/data/nat,int): add power to int, add trans attributes, power notation
|
2015-05-23 15:38:42 +10:00 |
|
Leonardo de Moura
|
e1c2340db2
|
fix(frontends/lean): consistent behavior for protected declarations
see https://github.com/leanprover/lean/issues/604#issuecomment-103265608
closes #609
|
2015-05-18 22:35:18 -07:00 |
|
Jeremy Avigad
|
8de6a4bb4c
|
feat(library/algebra/group_pow.lean,library/data/nat/power.lean): add generic power operation on monoids and groups
|
2015-05-13 22:19:02 -07:00 |
|
Jeremy Avigad
|
05e28aaf19
|
feat(library/data/nat/{basic.lean,order.lean}): use migrate
|
2015-05-12 06:20:51 -07:00 |
|
Jeremy Avigad
|
42616f766f
|
refactor(library/data/{nat,int,rat}/{basic.lean,order.lean}: make algebra instance declarations local
|
2015-05-12 06:20:47 -07:00 |
|
Leonardo de Moura
|
379af8a04e
|
feat(library): avoid 'definition' hack for theorems
|
2015-05-09 12:15:30 -07:00 |
|
Jeremy Avigad
|
7a1064b7e8
|
refactor(library/algebra/order.lean): rename a field in an order structure
|
2015-04-27 12:03:41 -07:00 |
|
Leonardo de Moura
|
072bf0b3b4
|
refactor(library): make sure "choose" compute inside the kernel
|
2015-04-25 23:10:48 -07:00 |
|
Leonardo de Moura
|
bf8a7eb9b4
|
fix(library/scoped_ext): bug in local metadata in sections
The problem is described in issue #554
|
2015-04-21 18:56:28 -07:00 |
|
Leonardo de Moura
|
754276a660
|
feat(frontends/lean): round parenthesis for [tactic1 | tactic2]
This commit also replaces the notation for divides
`(` a `|` b `)`
with
a `∣` b
The character `∣` is entered by typing \|
closes #516
|
2015-04-06 09:24:09 -07:00 |
|
Leonardo de Moura
|
4ec0e1b07c
|
feat(frontends/lean): improve calc mode
Now, it automatically supports transitivity of the form
(R a b) -> (b = c) -> R a c
(a = b) -> (R b c) -> R a c
closes #507
|
2015-04-04 08:58:35 -07:00 |
|
Leonardo de Moura
|
75621df52b
|
feat(frontends/lean): uniform notation for lists in tactics
closes #504
|
2015-03-27 17:54:48 -07:00 |
|
Jeremy Avigad
|
765f6f21f8
|
fix(library/algebra/ring.lean): allow degenerate semirings and rings, but not degenerate ordered_semirings and ordered_rings. Closes #478.
|
2015-03-25 18:29:06 -07:00 |
|
Leonardo de Moura
|
9b577a7b3e
|
feat(frontends/lean): add 'migrate' command
|
2015-03-14 21:48:00 -07:00 |
|
Leonardo de Moura
|
3c24461e51
|
refactor(*): modify '|' binding power, use 'abs a' instead of '|a|', and '(a | b)' instead of 'a | b'
|
2015-02-25 15:18:21 -08:00 |
|
Jeremy Avigad
|
cfdaffb6f5
|
feat/refactor(library/data/nat): do some housecleaning, add facts to div
|
2015-02-25 14:05:07 -08:00 |
|
Leonardo de Moura
|
a35cce38b3
|
feat(frontends/lean): new semantics for "protected" declarations
closes #426
|
2015-02-11 14:09:25 -08:00 |
|
Leonardo de Moura
|
2ffdbba8b0
|
feat(library): replace same 'calc' proofs with 'rewrite'
|
2015-02-05 10:39:25 -08:00 |
|
Jeremy Avigad
|
77e8439012
|
feat(library/data/nat/div): add theorems for coprime, etc.
|
2015-02-03 13:50:59 -08:00 |
|
Jeremy Avigad
|
95d79e7bda
|
refactor(library/data/nat): merge comm_semiring, make minor fixes
|
2015-02-01 11:17:44 -08:00 |
|
Jeremy Avigad
|
8d5a7a96b6
|
feat(library/data/nat/div): revise theorems, add lcm
|
2015-01-31 21:52:35 -08:00 |
|
Jeremy Avigad
|
928fc3ab81
|
feat(library/algebra/order,library/data/{nat,int}/order): make gt, ge reducible, add transitivity rules
|
2015-01-26 20:38:21 -05:00 |
|
Jeremy Avigad
|
0c04c7b0d2
|
fix(library/data/nat,int): make structure instances reducible
|
2015-01-26 20:38:21 -05:00 |
|
Jeremy Avigad
|
58057c5d99
|
feat(library/algebra/ordered_group): add abs
|
2015-01-21 15:46:17 -08:00 |
|
Leonardo de Moura
|
2e13e81fe0
|
refactor(library/data/nat/order): use record/structure instance expression
Motivation: do not rely on a specific argument ordering
|
2015-01-19 17:39:59 -08:00 |
|
Jeremy Avigad
|
b68ce77650
|
refactor/feat(library/data/nat): fix up sub and div, rename theorems, add theorems
|
2015-01-13 11:56:25 -05:00 |
|
Jeremy Avigad
|
0dcf06000b
|
refactor(library/data/int/sub): rename theorems, add theorems, clean up
|
2015-01-12 16:28:42 -05:00 |
|
Leonardo de Moura
|
1fab144aa7
|
refactor(library/init/nat): rename constants
closes #387
|
2015-01-07 18:26:51 -08:00 |
|
Jeremy Avigad
|
42c328e781
|
refactor(library/data/nat/basic): rename pred.zero and pred.succ
|
2015-01-07 18:18:28 -08:00 |
|
Jeremy Avigad
|
50f03c5a09
|
refactor(library/data/nat/order): make nat order an instance of linear_ordered_semigroup, rename various theorems
|
2015-01-07 18:18:28 -08:00 |
|
Jeremy Avigad
|
cecabbb401
|
refactor(library/data/int,library/algebra): make int an instnance of ordered ring, rename theorems
|
2014-12-26 16:25:05 -05:00 |
|
Jeremy Avigad
|
25394dddb7
|
refactor(library): change mul.left_id to mul_one, and similarly for mul.right_id, add.left_id, add.right_id
|
2014-12-23 21:14:36 -05:00 |
|
Jeremy Avigad
|
486bc321ff
|
refactor(library/data/nat): rename theorems
|
2014-12-23 21:14:35 -05:00 |
|
Jeremy Avigad
|
9d2587c79b
|
refactor(library/data/int/basic): make the integers an instance of ring
|
2014-12-17 13:32:38 -05:00 |
|