Leonardo de Moura
|
8c76419c60
|
fix(frontends/lean/decl_cmds): error localization problem for recursive equations
|
2015-03-30 13:30:29 -07:00 |
|
Leonardo de Moura
|
ec1a60b02c
|
feat(library/init/logic): add helper function for proving decidable equality
|
2015-03-30 02:14:26 -07:00 |
|
Soonho Kong
|
8243ed6339
|
fix(test*.sh): allow spaces in filename
fix #515
|
2015-03-28 23:29:52 -04:00 |
|
Leonardo de Moura
|
75621df52b
|
feat(frontends/lean): uniform notation for lists in tactics
closes #504
|
2015-03-27 17:54:48 -07:00 |
|
Leonardo de Moura
|
242f8ba048
|
feat(frontends/lean/elaborator): include number of unsolved goals
See #509
|
2015-03-27 14:54:41 -07:00 |
|
Leonardo de Moura
|
0c3fd7427e
|
feat(frontends/lean): add syntax-sugar for fold
closes #503
|
2015-03-25 18:25:48 -07:00 |
|
Leonardo de Moura
|
f2b1752807
|
fix(frontends/lean/parser): add workaround for #461
|
2015-03-25 18:09:43 -07:00 |
|
Leonardo de Moura
|
b9e3c474c9
|
feat(library/tactic): add all_goals tactic
closes #501
|
2015-03-25 17:42:34 -07:00 |
|
Leonardo de Moura
|
49bc56ec07
|
feat(frontends/lean/pp): improve pretty printer for prefix and postfix notation
closes #491
|
2015-03-25 16:45:58 -07:00 |
|
Leonardo de Moura
|
a1f933886f
|
fix(frontends/lean/structure_cmd): explicit universe levels for structures
closes #490
|
2015-03-25 16:10:30 -07:00 |
|
Leonardo de Moura
|
33d2e8d9d3
|
test(tests/lean/run): workaround for issue #505
|
2015-03-25 15:53:50 -07:00 |
|
Leonardo de Moura
|
5f1d827b26
|
fix(frontends/lean/decl_cmds): assertion violation
closes #506
|
2015-03-25 13:46:23 -07:00 |
|
Leonardo de Moura
|
ac30052a29
|
fix(library/tactic/rewrite_tactic): apply substitution before trying to rewrite
closes #487
|
2015-03-23 18:32:52 -07:00 |
|
Leonardo de Moura
|
5bf46d1226
|
fix(library/tactic/inversion_tactic): improve 'cases' tactic for HoTT mode
closes #481
|
2015-03-23 18:06:11 -07:00 |
|
Leonardo de Moura
|
76157ba392
|
fix(frontends/lean/pp): abbreviations with too much arguments
closes #480
|
2015-03-23 12:16:25 -07:00 |
|
Leonardo de Moura
|
0814e76298
|
fix(library/tactic/clear_tactic): unexpected failure
This commit also improves the error message produced by the 'clear' tactic.
fixes #488
|
2015-03-23 12:08:15 -07:00 |
|
Leonardo de Moura
|
35f2a61b4d
|
fix(tests/lean): add missing file
|
2015-03-23 11:35:39 -07:00 |
|
Leonardo de Moura
|
b5acbb2228
|
fix(frontends/lean/pp): missing parenthesis around abbreviations
fixes #476
|
2015-03-16 17:12:03 -07:00 |
|
Leonardo de Moura
|
fc3a7bac59
|
feat(frontends/lean): improve error handling inside match-with expressions
|
2015-03-13 23:25:46 -07:00 |
|
Leonardo de Moura
|
bed0d6df6b
|
fix(frontends/lean/elaborator): inaccessible over coercion
|
2015-03-13 23:04:45 -07:00 |
|
Leonardo de Moura
|
cfeb426cd7
|
fix(frontends/lean): pretty print numeral notation from algebra
|
2015-03-13 18:58:34 -07:00 |
|
Leonardo de Moura
|
362a0ec04c
|
test(tests/lean): tests for error handling improvements
|
2015-03-13 15:32:25 -07:00 |
|
Leonardo de Moura
|
b88b98ac22
|
feat(frontends/lean): try to add definition/theorem as axiom when it fails to be processed
The idea is to avoid a "tsunami" of error messages when a heavily used
theorem breaks in the beginning of the file
|
2015-03-13 14:47:21 -07:00 |
|
Leonardo de Moura
|
f5811d6092
|
feat(frontends/lean): hide subterms that do not contain metavariables
when generating "unresolved metavariables" error message
closes #473
|
2015-03-13 12:42:57 -07:00 |
|
Leonardo de Moura
|
cda19f5aa6
|
feat(library/tactic/rewrite_tactic): improve rewrite tactic error messages
closes #471
|
2015-03-12 20:49:53 -07:00 |
|
Leonardo de Moura
|
7accd0f1e6
|
feat(library/tactic/rewrite_tactic): allow rewrite with terms that contains binders
see discussion at #470
|
2015-03-12 18:07:55 -07:00 |
|
Leonardo de Moura
|
3e4d849a4a
|
refactor(kernel/metavar.h): simplify API
|
2015-03-12 12:50:53 -07:00 |
|
Leonardo de Moura
|
6a78ae7b46
|
fix(library/tactic/class_instance_synth): enforce consistent behavior in type class resolution
Auxiliary procedure mk_class_instance was not discarding partial solutions.
This procedure is used by the apply and inversion (aka cases) tactics
|
2015-03-12 10:27:05 -07:00 |
|
Leonardo de Moura
|
47a350d888
|
fix(library/tactic/inversion_tactic): missing condition for applying optimization
|
2015-03-12 09:11:36 -07:00 |
|
Leonardo de Moura
|
7de3d5771d
|
feat(library/tactic/rewrite_tactic): add eta-reduction support at esimp
closes #469
|
2015-03-12 00:32:31 -07:00 |
|
Leonardo de Moura
|
b5fb7c734e
|
feat(library/tactic/inversion_tactic): remove hypothesis being destructed
addresses second issue in #468
|
2015-03-11 20:42:50 -07:00 |
|
Leonardo de Moura
|
4c6b0dc0e5
|
fix(library/tactic/expr_to_tactic): tactic_expr_to_id did not take as_atomic annotation into account
fixes #466
|
2015-03-11 08:49:59 -07:00 |
|
Leonardo de Moura
|
4904f7657f
|
test(tests/lean/run): add definition package tests
|
2015-03-09 08:42:21 -07:00 |
|
Leonardo de Moura
|
f6cd604a44
|
chore(library/data/bool): enforce naming conventions
|
2015-03-06 19:20:48 -08:00 |
|
Leonardo de Moura
|
f966634910
|
feat(frontends/lean): nested dependent pattern matching
|
2015-03-06 19:18:08 -08:00 |
|
Leonardo de Moura
|
14ca2d407d
|
test(tests/lean/run): add match-with nested in tactic test
|
2015-03-06 17:47:01 -08:00 |
|
Leonardo de Moura
|
1490bdad49
|
feat(frontends/lean): add version of 'exact' tactic (sexact) that enforces goal type during term elaboration
|
2015-03-06 17:34:45 -08:00 |
|
Leonardo de Moura
|
bd8c4315f1
|
feat(frontends/lean): allow 'match-with' to be used in tactics without prefixing it with 'exact'
|
2015-03-06 15:49:31 -08:00 |
|
Leonardo de Moura
|
4edd7b9099
|
fix(library/definitional/equations): allow a function to be the result of a match-with term or recursive definition
|
2015-03-06 15:08:52 -08:00 |
|
Leonardo de Moura
|
f24d9e84fe
|
feat(frontends/lean): add option 'max_memory'
Default value is 512Mb
|
2015-03-06 13:56:20 -08:00 |
|
Leonardo de Moura
|
3b721fe675
|
feat(frontends/lean): add missing 'help' command
|
2015-03-06 13:56:20 -08:00 |
|
Leonardo de Moura
|
daf36803c4
|
fix(frontends/lean/builtin_exprs): bug in 'using' construct
|
2015-03-06 13:56:20 -08:00 |
|
Leonardo de Moura
|
368f9d347e
|
refactor(frontends/lean): approach used to parse tactics
The previous approach was too fragile
TODO: we should add separate parsing tables for tactics
|
2015-03-05 18:11:21 -08:00 |
|
Leonardo de Moura
|
28487ede3b
|
feat(frontends/lean/decl_cmds): allow 'empty' set of pattern matching equations
|
2015-03-05 14:37:29 -08:00 |
|
Leonardo de Moura
|
b73a931c70
|
fix(frontends/lean/elaborator): missing case 'no-equation' annotation
|
2015-03-05 14:37:29 -08:00 |
|
Leonardo de Moura
|
039afb4578
|
feat(frontends/lean): treat "proof t qed" as alias for "by exact t"
|
2015-03-05 11:12:39 -08:00 |
|
Leonardo de Moura
|
abd238aef0
|
feat(*): add [quasireducible] attribute
|
2015-03-04 22:12:49 -08:00 |
|
Leonardo de Moura
|
c6d15dc198
|
fix(tests/lean/interactive): adjust tests to reflect changes in the standard library
|
2015-03-04 18:30:31 -08:00 |
|
Leonardo de Moura
|
fde83cd376
|
fix(tests/lean/hott): adjust tests to reflect changes in the libraries
|
2015-03-04 09:28:16 -08:00 |
|
Leonardo de Moura
|
18e6e55fc9
|
chore(tests/lean/interactive/num2): adjust test to reflect changes in the standard library
|
2015-03-03 16:17:59 -08:00 |
|