Rob Lewis
|
2273dc669e
|
feat(library/data): fill in sorrys in int and rat orderings
|
2015-05-29 14:11:51 +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
|
5da4922397
|
feat(library/data/list/perm): cleanup proofs
refl and symm were refering to the setoid.refl and setoid.symm.
Moreover, they were producing harder elaboration problems
|
2015-05-27 12:30:56 -07:00 |
|
Leonardo de Moura
|
47e5633498
|
feat(frontends/lean/calc_proof_elaborator): avoid unnecessary unfolding in the calc tactic
|
2015-05-27 12:07:39 -07:00 |
|
Floris van Doorn
|
0c7e16e017
|
feat(library.data.int.basic): move theorems about successor and predecessor from HoTT to standard library
|
2015-05-26 21:37:01 -07:00 |
|
Leonardo de Moura
|
7f0951b8e7
|
feat(library/tactic): improve assumption tactic performance
|
2015-05-25 20:22:37 -07:00 |
|
Rob Lewis
|
393cefcf97
|
feat(library/data/real): define real numbers, prove they form a commutative ring
|
2015-05-26 12:05:53 +10:00 |
|
Rob Lewis
|
681f431d4b
|
feat(library/data/rat): make rat subtraction reducible, fix migration of min/max
|
2015-05-26 11:52:34 +10: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
|
a64c0ea845
|
feat/refactor(library/data/{int,rat}/*): improve casting from nat to int to rat
|
2015-05-25 16:50:42 -07:00 |
|
Jeremy Avigad
|
4ed9e46532
|
refactor(library/data/int/*): use better direction for of_nat theorems
|
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
|
7c92161e49
|
refactor(library/data/finset/basic.lean): change order of arguments to induction tactic
|
2015-05-25 16:50:42 -07:00 |
|
Leonardo de Moura
|
6db08c5519
|
test(library): test new tactics in the standard library
|
2015-05-25 16:48:33 -07:00 |
|
Leonardo de Moura
|
7e875c8d85
|
refactor(library): simplify theorems using improved tactics
|
2015-05-25 10:43:28 -07:00 |
|
Leonardo de Moura
|
88975927e6
|
fix(library/tactic/relation_tactics): beta-reduce goal before trying to extract head symbol
|
2015-05-24 18:56:35 -07:00 |
|
Leonardo de Moura
|
c453bb52a9
|
feat(library/data/stream): add notation and commonly used definitions
|
2015-05-24 16:53:58 -07:00 |
|
Leonardo de Moura
|
880027ea0e
|
feat(library/data/stream): define stream mem predicate and prove basic theorems
|
2015-05-24 15:47:33 -07:00 |
|
Leonardo de Moura
|
607a5fbb86
|
feat(library/data/stream): define cycle, inits, tails for streams and prove basic theorems
|
2015-05-24 13:42:51 -07:00 |
|
Leonardo de Moura
|
3181471024
|
feat(library/data/list/basic): add nth_eq_some aux theorem
|
2015-05-24 10:10:23 -07:00 |
|
Leonardo de Moura
|
32a2425e02
|
feat(library/data/stream): prove take lemma for infinite streams
|
2015-05-23 23:01:54 -07:00 |
|
Leonardo de Moura
|
75901157a1
|
feat(library/data/stream): add more declarations and examples demonstrating how to use eq_of_bisim
|
2015-05-23 22:03:17 -07:00 |
|
Leonardo de Moura
|
d987d6cc84
|
feat(library/data/stream): simplify corecursion proofs, define interleave operation by corecursion, add one example of proof by bisimulation
|
2015-05-23 16:00:08 -07:00 |
|
Leonardo de Moura
|
8685e8ad7e
|
feat(library/data/stream): define corec for infinite streams
|
2015-05-23 14:32:52 -07:00 |
|
Leonardo de Moura
|
dd4dd154ec
|
feat(library/data/stream): add bisimulation for streams
|
2015-05-23 12:07:27 -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 |
|
Jeremy Avigad
|
a662f925cb
|
refactor(library/data/quotient.lean): improve comments
|
2015-05-23 14:21:16 +10:00 |
|
Jeremy Avigad
|
4bc93b59e3
|
feat(library/data/rat/{basic,order}.lean): add property of of_int
|
2015-05-23 12:34:07 +10:00 |
|
Jeremy Avigad
|
59c1801921
|
refactor(library/data/{list,set,finset}/basic.lean): make subset reserved notation
|
2015-05-23 12:34:07 +10:00 |
|
Leonardo de Moura
|
fe32b9fa7f
|
feat(library/data/stream): add infinite streams
|
2015-05-22 18:08:11 -07:00 |
|
Leonardo de Moura
|
1665ee39e8
|
feat(library/data/finset/card): test 'induction' tactic at finset
|
2015-05-19 15:56:51 -07:00 |
|
Leonardo de Moura
|
3e87f09d78
|
feat(library/tactic/induction_tactic): add support for user-defined recursors that contain parameters that should be synthesized by type class resolution
|
2015-05-19 15:33:46 -07: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 |
|
Floris van Doorn
|
2144036cdb
|
feat(hott.circle): prove that the fundamental group of the circle is equal to the integers, as groups
Also many minor fixes at various places
|
2015-05-18 15:59:55 -07:00 |
|
Leonardo de Moura
|
19361f0196
|
feat(library/unifier): do not fire type class resolution as last resort when type contains metavariables
see discussion at #604
|
2015-05-18 15:45:23 -07:00 |
|
Jeremy Avigad
|
566acf4b31
|
feat(library/data/finset/card.lean): add card_Union_of_disjoint and other theorems
|
2015-05-17 19:06:10 +10:00 |
|
Jeremy Avigad
|
6549940c63
|
feat(library/data/finset/bigops.lean): add Union for finsets
|
2015-05-17 17:50:32 +10:00 |
|
Jeremy Avigad
|
783dd61083
|
feat(library/data/finset/basic.lean): add useful calculation rules for quantifiers
|
2015-05-17 17:49:02 +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
|
981bf93ce0
|
feat(library/data/default.lean): add rat and vector
|
2015-05-17 12:19:47 +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
|
63bb4b558a
|
fix(library/data/set/{classical_inverse.lean,map.lean}): protect definitions in map, to avoid ambiguity
|
2015-05-16 18:24:19 +10:00 |
|
Jeremy Avigad
|
26ad6dde69
|
fix(library/data/fintype.lean): reduce imports, to avoid cyclic dependencies
|
2015-05-16 17:53:35 +10:00 |
|
Jeremy Avigad
|
81d0d4aa53
|
fix(library/data/{set,finset}/basic.lean: delete \{{ \}}} notation (conflicts with records)
|
2015-05-16 17:53:35 +10:00 |
|