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
|
8bebd104ff
|
refactor(library/*): remove 'Module:' lines
|
2015-05-23 20:52:23 +10: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
|
6549940c63
|
feat(library/data/finset/bigops.lean): add Union for finsets
|
2015-05-17 17:50:32 +10:00 |
|
Jeremy Avigad
|
9720d84095
|
refactor(library/algebra/group_bigops.lean,library/data/nat/bigops.lean): add ext principle, clean up file
|
2015-05-17 16:00:38 +10:00 |
|
Jeremy Avigad
|
4764f6e8ec
|
refactor(library/algebra/group_bigops.lean,library/data/nat/bigops.lean): simplify naming scheme for bigops
|
2015-05-17 15:24:37 +10:00 |
|
Jeremy Avigad
|
ff701a9812
|
feat(library/data/nat/bigops.lean): add finite products and sums for nat
|
2015-05-16 22:26:59 +10:00 |
|
Jeremy Avigad
|
eae047bd31
|
refactor,feat(library/{data,algebra}): move bigops to algebra, define sums
|
2015-05-16 18:42:13 +10: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 |
|
Leonardo de Moura
|
9760968b45
|
refactor(library,hott): use/test new 'contradiction' tactic in the standard and hott libraries
|
2015-04-30 13:56:12 -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
|
670eac9d50
|
refactor(library): avoid 'context' command in the standard library
|
2015-04-21 19:13:19 -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
|
cc63a40a01
|
feat(library): enforce name conventions on old nat declarations
|
2015-04-18 10:50:30 -07:00 |
|
Leonardo de Moura
|
7a4f43d6ab
|
feat(library/data/nat/choose): choice function for natural numbers
|
2015-04-16 11:33:26 -07:00 |
|
Leonardo de Moura
|
a7db8a2bac
|
theorem(library/data/countable): prove that the product of two countable types is countable
|
2015-04-14 20:39:58 -07:00 |
|
Leonardo de Moura
|
38b880b939
|
feat(library/data/nat/pairing): add unpair_mkpair theorem
|
2015-04-14 20:28:20 -07:00 |
|
Leonardo de Moura
|
f7a43c7997
|
feat(library/data/nat/sqrt): generalize sqrt_eq theorem
|
2015-04-14 20:10:18 -07:00 |
|
Leonardo de Moura
|
faca0acd26
|
feat(library/data/nat/sqrt): add sqrt_eq theorem
|
2015-04-14 15:38:54 -07:00 |
|
Leonardo de Moura
|
11dbcda9d2
|
feat(library/data/nat/pairing): add "elegant" pairing/unpairing function
|
2015-04-14 09:01:15 -07:00 |
|
Leonardo de Moura
|
2eb7538c96
|
fix(library/data/nat/sqrt): adjust to reflect recent changes
|
2015-04-14 09:01:15 -07:00 |
|
Leonardo de Moura
|
4180b80df6
|
feat(library/data/nat/power): define power and add basic theorems
|
2015-04-14 09:01:15 -07:00 |
|
Leonardo de Moura
|
ff72a520ff
|
feat(library/data/nat/div): add mul_cancel theorems
|
2015-04-14 09:01:15 -07:00 |
|
Leonardo de Moura
|
c73c1dbb63
|
feat(library/data/nat/sub): add two extra theorems
|
2015-04-14 09:01:15 -07:00 |
|
Leonardo de Moura
|
11c9bb4626
|
feat(library/data/nat): naive square root function
|
2015-04-14 09:01:15 -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 |
|
Jeremy Avigad
|
ec05e83a2a
|
feat(library/data/int/div.lean): add theorems about div
|
2015-03-12 20:54:49 -07:00 |
|
Leonardo de Moura
|
df13588b93
|
chore(library/data): remove unnecessary parentheses
|
2015-03-01 14:18:36 -08: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 |
|
Leonardo de Moura
|
c04c610b7b
|
feat(frontends/lean): add 'assert H : A, ...' as notation for 'have H [visible] : A, ...'
|
2015-02-25 14:30:42 -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
|
3ede8e9150
|
refactor(library): use [] binder annotation when declaring instances
|
2015-02-24 16:12:39 -08:00 |
|
Leonardo de Moura
|
1cd44e894b
|
feat(library/tactic/class_instance_synth): conservative class-instance resolution: expand only definitions marked as reducible
closes #442
|
2015-02-24 16:12:35 -08:00 |
|
Leonardo de Moura
|
74b8499fa9
|
refactor(library/data/nat/div): simplify proof of dvd_of_dvd_add_left
|
2015-02-17 18:55:44 -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 |
|