Leonardo de Moura
|
ca110012d8
|
feat(library/tactic): automate "generalize-intro-induction/cases" idiom
closes #645
|
2015-05-30 21:57:28 -07:00 |
|
Leonardo de Moura
|
e5a82ef516
|
feat(frontends/lean): add option for disabling "coercion lifting"
|
2015-05-30 17:07:42 -07:00 |
|
Leonardo de Moura
|
6f6848968d
|
feat(frontends/lean/coercion_elaborator): "coercion lifting" for backtracking case
closes #252
|
2015-05-30 16:44:26 -07:00 |
|
Leonardo de Moura
|
ea9c810fca
|
feat(frontends/lean/coercion_elaborator): implement "coercion lifting"
closes #644
|
2015-05-30 14:45:14 -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 |
|
Jeremy Avigad
|
c986ee305b
|
refactor(library/data/nat/gcd.lean): move gcd to a new file
|
2015-05-30 22:10:21 +10:00 |
|
Jeremy Avigad
|
cc0a620db1
|
feat(library/data/{nat,int}/div.lean): add to and improve div library
|
2015-05-30 22:10:21 +10:00 |
|
Leonardo de Moura
|
6d2f37857d
|
feat(frontends/lean/builtin_cmds): add 'print [reducible]', 'print [irreducible]' and 'print [quasireducible]' commands
|
2015-05-29 16:47:29 -07:00 |
|
Leonardo de Moura
|
7a0e198147
|
feat(kernel,frontends/lean/builtin_cmds): allow kernel extensions to report their builtin constants
|
2015-05-29 16:28:16 -07:00 |
|
Leonardo de Moura
|
c07d14e94a
|
fix(library/tactic/rewrite_tactic): incorrect assertion
|
2015-05-29 15:59:03 -07:00 |
|
Leonardo de Moura
|
0ceedbe69e
|
fix(library/normalize): fixes #640
|
2015-05-29 15:58:59 -07:00 |
|
Leonardo de Moura
|
60ff057159
|
test(tests/lean): add missing test for issue #634
|
2015-05-29 15:13:43 -07:00 |
|
Leonardo de Moura
|
f48cdccd20
|
fix(frontends/lean/pp): abbreviation with parameters
closes #639
|
2015-05-29 15:13:31 -07:00 |
|
Leonardo de Moura
|
a071012346
|
fix(frontends/lean/pp,library/head_map): handle 'as_atomic' annotation
This commit fixes local notation that contains parameters
see issue #639
|
2015-05-29 14:51:28 -07:00 |
|
Leonardo de Moura
|
e6099583ad
|
feat(frontends/lean/builtin_cmds): expand abbreviations in the 'check' command
see issue #639
|
2015-05-29 14:51:07 -07:00 |
|
Leonardo de Moura
|
3b7b268e40
|
fix(frontends/lean/pp): fixes #634
trying again...
|
2015-05-29 14:07:38 -07:00 |
|
Leonardo de Moura
|
7f12401ea7
|
fix(frontends/lean/elaborator): save type information for 'obtain' declarations
|
2015-05-29 10:16:12 -07:00 |
|
Rob Lewis
|
82f85a574d
|
feat(library/data/real): prove reals form an ordered ring
|
2015-05-29 14:11:51 +10:00 |
|
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 |
|
Rob Lewis
|
4b67cd1f97
|
feat(library/algebra): update algebraic hierarchy to be more constructive
|
2015-05-29 14:11:50 +10:00 |
|
Leonardo de Moura
|
7342f342a9
|
fix(frontends/lean/pp): fixes #634
|
2015-05-28 19:43:49 -07:00 |
|
Leonardo de Moura
|
ae0bdaa836
|
chore(library,util): fix style
|
2015-05-27 16:46:58 -07:00 |
|
Leonardo de Moura
|
d95c064a29
|
feat(library/simplifier/ceqv): add to_ceqv procedure
|
2015-05-27 16:35:56 -07:00 |
|
Leonardo de Moura
|
00232e70d6
|
feat(hott,library): auxiliary theorems for simplifier
|
2015-05-27 16:35:56 -07:00 |
|
Leonardo de Moura
|
85409a59d3
|
feat(library/tactic/rewrite_tactic): add xrewrite and krewrite tactic variants
closes #511
|
2015-05-27 16:32:43 -07:00 |
|
Leonardo de Moura
|
7d73f4f091
|
refactor(library,frontends/lean): simplify the creation of custom normalizers
|
2015-05-27 15:33:20 -07: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 |
|
Leonardo de Moura
|
77f742ae8e
|
feat(library/relation_manager): add auxiliary functions
|
2015-05-27 12:07:06 -07:00 |
|
Leonardo de Moura
|
4867dba175
|
fix(util/stackinfo): saving max stack size on OSX
see issue #628
|
2015-05-27 08:52:39 -07:00 |
|
Leonardo de Moura
|
ea43f3ea80
|
fix(frontends/lean/builtin_cmds): fixes #630
|
2015-05-26 22:19:42 -07:00 |
|
Floris van Doorn
|
96a4a015d9
|
fix(hit): make the nondependent eliminator standard for hits
|
2015-05-26 21:37:02 -07:00 |
|
Floris van Doorn
|
a127a676eb
|
fix(tests): fix tests to reflect changes
|
2015-05-26 21:37:02 -07:00 |
|
Floris van Doorn
|
43bcdd7994
|
feat(hott): remove sorry's in circle.hlean, characterize pathovers in degenerate pi's
|
2015-05-26 21:37:01 -07:00 |
|
Floris van Doorn
|
c64d73aae4
|
feat(types.nat): prove that inequalities on nat are mere propositions
Also some small changes in various other locations
|
2015-05-26 21:37:01 -07:00 |
|
Floris van Doorn
|
95e0fbb71a
|
feat(hott): add interval and (start of) squareovers
|
2015-05-26 21:37:01 -07:00 |
|
Floris van Doorn
|
d7c1a8f2e0
|
feat(hott): small fixes in hit and cubical.square
|
2015-05-26 21:37:01 -07:00 |
|
Floris van Doorn
|
4a29f4bdd4
|
feat(types): incorporate pathovers in the files of the types folder
Conflicts:
hott/cubical/pathover.hlean
|
2015-05-26 21:37:01 -07:00 |
|
Floris van Doorn
|
0b12d51b25
|
feat(hott): use pathovers in all the recursors of hits
move pathover file to the init folder
|
2015-05-26 21:37:01 -07:00 |
|
Floris van Doorn
|
54ed8a8e76
|
feat(hott): small changes in init and category
|
2015-05-26 21:37:01 -07:00 |
|
Floris van Doorn
|
8396c4c824
|
feat(lean-syntax): color abbreviations yellow
|
2015-05-26 21:37:01 -07:00 |
|
Floris van Doorn
|
40d5f83851
|
feat(hit): start using induction tactic
|
2015-05-26 21:37:01 -07:00 |
|
Floris van Doorn
|
50290fb81c
|
feat(hott): add recursor attribute to hits
recursor attribute is added to both the dependent and nondependent elimination, is such a way that the dependent elimination is used by default
|
2015-05-26 21:37:01 -07:00 |
|
Floris van Doorn
|
8056f326d7
|
feat(reserved_notation): make is_typeof parsing-only, add ^ to HoTT
|
2015-05-26 21:37:01 -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
|
4d1b711247
|
feat(frontends/lean/elaborator): better error localization when running out of stack space and/or memory in begin-end tactic mode.
|
2015-05-26 20:09:15 -07:00 |
|
Soonho Kong
|
c4ec89ae6d
|
fix(emacs/lean-flycheck.el): use -concat in lean-flycheck-command
|
2015-05-26 17:00:05 -04:00 |
|
Soonho Kong
|
1d25f9fa06
|
fix(emacs/lean-util.el): use f-join instead of lean-concat-paths
|
2015-05-26 17:00:05 -04:00 |
|