Leonardo de Moura
|
c772d7bf84
|
fix(frontends/lean/elaborator): unassigned metavariable when using nested begin-end blocks
Closes #454
|
2015-02-28 09:03:56 -08:00 |
|
Leonardo de Moura
|
cf56935b01
|
feat(frontends/lean): improve support for user defined tactics
|
2015-02-27 16:58:25 -08:00 |
|
Leonardo de Moura
|
5b736a2268
|
feat(frontends/lean): add support for empty match-with expressions
|
2015-02-26 16:36:15 -08:00 |
|
Leonardo de Moura
|
68110faa4d
|
feat(frontends/lean/inductive_cmd): allow '|' in inductive datatype declarations
|
2015-02-25 17:00:10 -08:00 |
|
Leonardo de Moura
|
5ca52d81ec
|
feat(frontends/lean): ML-like notation for match and recursive equations
|
2015-02-25 16:20:44 -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
|
e555531eb6
|
feat(library/data/int/div): start on div for integers
|
2015-02-25 14:05:07 -08:00 |
|
Leonardo de Moura
|
96b54a8007
|
feat(frontends/lean/builtin_exprs): add 'have' notation in 'begin-end' blocks
It is notation for the assert tactic.
|
2015-02-25 14:04:17 -08:00 |
|
Leonardo de Moura
|
909ebfc5f1
|
feat(frontends/lean/elaborator): try coercions after each overload
We try only the easy cases since the more general case is too expensive.
closes #444
|
2015-02-24 17:41:20 -08:00 |
|
Leonardo de Moura
|
34c36648bb
|
fix(frontends/lean/decl_cmds): constants command
closes #445
|
2015-02-24 16:27:13 -08:00 |
|
Leonardo de Moura
|
42289d4334
|
feat(library/tactic/class_instance_synth): create class instance synthesis subproblems only for arguments marked with the [] binder annotation
|
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
|
1ff6446a63
|
feat(frontends/lean): nested begin-end blocks
|
2015-02-24 11:59:27 -08:00 |
|
Leonardo de Moura
|
dc2ac92846
|
fix(library/definitional/equations): use whnf on recursive definition arguments
The idea is to expose "hidden" datatypes.
|
2015-02-23 22:27:30 -08:00 |
|
Leonardo de Moura
|
7adecaf494
|
fix(frontends/lean/structure_cmd): include context/section parameteres/variables that are used in explicit structure parameters
|
2015-02-23 15:28:43 -08:00 |
|
Leonardo de Moura
|
7d35d18cad
|
fix(library/tactic/rewrite_tactic): bug when matching terms that expanded into projections
|
2015-02-22 18:23:10 -08:00 |
|
Leonardo de Moura
|
33e562a7ce
|
fix(frontends/lean/structure_cmd): effect of "include" command in the structure command
closes #438
|
2015-02-19 22:44:51 -08:00 |
|
Leonardo de Moura
|
4248ad644d
|
fix(frontends/lean): priority expressions parser
|
2015-02-14 12:26:06 -08:00 |
|
Leonardo de Moura
|
8ffadce4ab
|
feat(frontends/lean): add "premise" and "premises" command
It is just an alternative notation for "variable" and "variables"
closes #429
|
2015-02-11 18:46:03 -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
|
1832fb6f54
|
feat(*): uniform metaclass names, metaclass validation at 'open' command
|
2015-02-11 10:35:04 -08:00 |
|
Leonardo de Moura
|
9d1cd073c5
|
feat(frontends/lean): add 'print metaclasses' command
|
2015-02-11 10:13:20 -08:00 |
|
Leonardo de Moura
|
2126b8ec9a
|
feat(library/tactic/apply_tactic): perform class-instance resolution in the apply tactic
closes #360
|
2015-02-06 16:14:03 -08:00 |
|
Leonardo de Moura
|
1e8a975daa
|
feat(frontends/lean): extend parser: rewrite "fold" step
|
2015-02-06 15:22:34 -08:00 |
|
Leonardo de Moura
|
04f8278c90
|
test(tests/lean/run): add rewrite tactic test
|
2015-02-06 14:14:42 -08:00 |
|
Leonardo de Moura
|
5b25da8c43
|
feat(frontends/lean): add esimp tactic based on rewrite tactic
closes #358
|
2015-02-06 14:13:32 -08:00 |
|
Leonardo de Moura
|
b4139627e5
|
feat(library/tactic/rewrite_tactic): add option to prevent any kind of constant unfolding when perfoming pattern matching in the rewrite tactic
|
2015-02-06 13:27:33 -08:00 |
|
Leonardo de Moura
|
78bde6c9e6
|
test(tests/lean/run): add more rewrite tactic tests
|
2015-02-06 12:57:42 -08:00 |
|
Leonardo de Moura
|
2e626b29fb
|
feat(library/tactic/rewrite_tactic): allow many constants to be provided in a single rewrite unfold step
|
2015-02-06 11:03:36 -08:00 |
|
Leonardo de Moura
|
56a46ae61e
|
feat(frontends/lean/parse_tactic_location): make rewrite notation more uniform
|
2015-02-06 10:31:50 -08:00 |
|
Leonardo de Moura
|
e17ba27596
|
fix(library/tactic/rewrite_tactic): adjust the behavior of class resolution in rewriter
The solution is not very satisfactory. I should investigate it more.
|
2015-02-05 19:08:47 -08:00 |
|
Leonardo de Moura
|
e097977bac
|
test(tests/lean/run): add more rewrite tactic tests
|
2015-02-05 14:09:07 -08:00 |
|
Leonardo de Moura
|
ffe0d1186e
|
feat(library/tactic/rewrite_tactic): add "reduce_to" step at rewrite tactic
|
2015-02-05 13:59:55 -08:00 |
|
Leonardo de Moura
|
116c65bff5
|
feat(library/tactic/rewrite_tactic): add reduction step to rewrite tactic
|
2015-02-05 13:42:50 -08:00 |
|
Leonardo de Moura
|
808521223b
|
feat(library/tactic/rewrite_tactic): support constant unfolding in rewrite tactic
|
2015-02-05 12:58:30 -08:00 |
|
Leonardo de Moura
|
1b73764ad3
|
fix(tests/lean/run/elim2): adjust test to reflect recent changes
|
2015-02-05 10:54:00 -08:00 |
|
Leonardo de Moura
|
d6958be7e7
|
fix(library/tactic/location): replace cache must not be used when only a subset of all occurrences should be replaced at replace_occurrences
|
2015-02-05 10:50:40 -08:00 |
|
Leonardo de Moura
|
dfad24e3f5
|
feat(frontends/lean): polish rewrite tactic notation
|
2015-02-05 10:15:58 -08:00 |
|
Leonardo de Moura
|
0abfa30ead
|
fix(library/tactic/rewrite_tactic): elaboration bug in the rewrite tactic steps/elements
|
2015-02-05 10:01:18 -08:00 |
|
Leonardo de Moura
|
15efadfbdc
|
feat(frontends/lean/parse_rewrite_tactic): cleanup rewrite tactic notation
Make a rewrite command sequence explicit.
|
2015-02-04 20:16:24 -08:00 |
|
Leonardo de Moura
|
14c72e82f6
|
feat(library/tactic/rewrite_tactic): add support for rewriting hypotheses
|
2015-02-04 20:04:19 -08:00 |
|
Leonardo de Moura
|
d0171ffe7a
|
test(tests/lean/run): add more rewrite tactic examples
|
2015-02-04 19:19:46 -08:00 |
|
Leonardo de Moura
|
0c8eaa38c8
|
test(tests/lean/run): add basic rewriter test
|
2015-02-04 15:30:18 -08:00 |
|
Leonardo de Moura
|
f79f43c702
|
refactor(library/match): use "special" meta-variables instead of free variables to represent placholders in the higher-order matcher
|
2015-02-03 15:15:04 -08:00 |
|
Leonardo de Moura
|
3f37c0e739
|
test(tests/lean/run): add 'export' command test
|
2015-02-01 19:57:26 -08:00 |
|
Leonardo de Moura
|
6cd4972a84
|
fix(tests/lean): adjust tests to reflect changes in the standard library
|
2015-02-01 11:36:38 -08:00 |
|
Leonardo de Moura
|
15716c1471
|
feat(frontends/lean/calc_proof_elaborator): reject proofs with metavariables in the calc-assistant
|
2015-02-01 11:11:27 -08:00 |
|
Leonardo de Moura
|
143143e94c
|
fix(library/tactic/inversion_tactic): missing normalization step in the inversion_tactic
|
2015-02-01 10:38:30 -08:00 |
|
Leonardo de Moura
|
d52af105d7
|
feat(frontends/lean/decl_cmds): allow many constants to be set in the same attribute command
|
2015-01-31 23:55:14 -08:00 |
|