Leonardo de Moura
e379034b95
feat(library/tactic): improve 'assumption' tactic
...
- It uses the unifier in "conservative" mode
- It only affects the current goal
closes #570
2015-05-02 17:33:54 -07:00
Leonardo de Moura
8c107d6936
fix(frontends/lean/builtin_cmds): bug in export
command
...
Cause: we have two different tokes to represent declarations: [decls] and [declarations]
fixes #568
2015-05-02 16:01:25 -07:00
Leonardo de Moura
b39fe17dee
feat(library/tactic): add 'transitiviy', 'reflexivity' and 'symmetry' tactics
...
closes #500
2015-05-02 15:48:25 -07:00
Leonardo de Moura
cd17618f4a
refactor(library): replace 'calc_trans', 'calc_symm', 'calc_refl' and 'calc_subst' commands with attributes '[symm]', '[refl]', '[trans]' and '[subst]'
...
These attributes are used by the calc command.
They will also be used by tactics such as 'reflexivity', 'symmetry' and
'transitivity'.
See issue #500
2015-05-02 15:15:35 -07:00
Leonardo de Moura
efc33a2f1d
fix(tests/lean): adjusts tests
2015-05-02 13:01:37 -07:00
Leonardo de Moura
415ca2b93f
feat(library/tactic): add 'congruence' tactic
...
It is the f_equal described at issue #500 .
2015-05-02 12:58:46 -07:00
Leonardo de Moura
230b994e79
fix(tests/lean/slow): adjust tests
2015-05-01 19:47:55 -07:00
Leonardo de Moura
9dc0388022
fix(library/tactic/rewrite_tactic): bug when rewriting hypotheses
2015-05-01 19:45:23 -07:00
Leonardo de Moura
ac8ba6a3cf
feat(library/tactic): add 'subst' tactic
...
see issue #500
2015-05-01 19:31:24 -07:00
Leonardo de Moura
b0759f3986
fix(library/tactic/rewrite_tactic): bug when rewriting multiple hypotheses
2015-05-01 19:03:43 -07:00
Leonardo de Moura
ea87dd48e3
chore(tests/lean/hott/inj_tac): fix typo
2015-05-01 18:18:57 -07:00
Leonardo de Moura
de369a0a0a
feat(library/tactic/injection_tactic): improve 'injection' tactic
...
see issue #500
2015-05-01 15:49:56 -07:00
Leonardo de Moura
9ba8b284a1
fix(library/tactic/apply_tactic): add eapply, and fix issue #361
2015-05-01 15:08:00 -07:00
Leonardo de Moura
63eb155c7e
feat(library/tactic): add 'injection' tactic
...
see issue #500
2015-05-01 12:45:21 -07:00
Leonardo de Moura
7e9f574ef3
fix(library/tactic/apply_tactic): use internally 'apply' instead of 'fapply' as the default "apply" tactic
...
This changes improves the 'constructor' tactic
2015-04-30 21:58:35 -07:00
Leonardo de Moura
4f7f66de3f
test(tests/lean/run): add new test
2015-04-30 21:38:33 -07:00
Leonardo de Moura
2d9c950144
feat(library/tactic/constructor_tactic): allow 'constructor' tactic without index
...
see issue #500
2015-04-30 21:15:07 -07:00
Leonardo de Moura
15e52b06df
fix(library/tactic/constructor_tactic): bug in constructor tactic
...
see example (constr_tac2.lean) in comment at issue #500
2015-04-30 20:18:24 -07:00
Leonardo de Moura
d18f9c7607
fix(library/tactic/constructor_tactic): use 1 (instead of 0) to reference the first constructor
...
see comment at issue #500
2015-04-30 20:08:00 -07:00
Leonardo de Moura
0b995c4fe3
fix(library/tactic/rewrite_tactic): relax reducibility constraints in some parts of the rewrite tactic
...
fixes #567
2015-04-30 18:22:58 -07:00
Leonardo de Moura
d152f38518
feat(library/tactic): add 'constructor', 'split', 'left', 'right' and 'existsi' tactics
...
see issue #500
2015-04-30 17:52:29 -07:00
Leonardo de Moura
125ab8c228
fix(tests/lean/interactive/findp): adjust test output
2015-04-30 15:45:15 -07:00
Leonardo de Moura
1c6067bac2
feat(library/tactic): add 'exfalso' tactic
...
see issue #500
2015-04-30 15:43:07 -07:00
Leonardo de Moura
9c8a63caec
feat(library/tactic): add 'contradiction' tactic
...
see issue #500
Remark: this tactic also applies no_confusion to take care of a contradiction
2015-04-30 13:47:40 -07:00
Leonardo de Moura
3233008039
feat(library/tactic): allow user to name generalized term in the 'generalize' tactic
...
closes #421
2015-04-30 11:57:40 -07:00
Leonardo de Moura
3912bc24c8
feat(frontends/lean): nicer syntax for 'intros' 'reverts' and 'clears'
2015-04-30 11:00:39 -07:00
Leonardo de Moura
d6d30f12c6
feat(frontends/lean): add "polymorphic" print command
...
closes #524
2015-04-29 16:17:33 -07:00
Leonardo de Moura
1a28a3c36f
feat(frontends/lean): add 'print inductive' command
2015-04-29 15:22:10 -07:00
Leonardo de Moura
dce7177382
feat(library/tactic/change_tactic): improve 'change' tactic
...
- Better error messages
- Try to solve unification constraints produced during is_def_eq test
addresses comment on issue #531
2015-04-29 13:31:09 -07:00
Leonardo de Moura
d055947243
feat(library/tactic/rewrite_tactic): ignore implicit argument when matching at rewrite tactic
2015-04-29 12:51:33 -07:00
Leonardo de Moura
b790ca9806
fix(library/tactic/rewrite_tactic): type check rewriting steps
...
closes #550
2015-04-29 12:16:37 -07:00
Leonardo de Moura
d1cb0018c0
fix(tests): adjust tests to reflect changes in the HoTT library
2015-04-29 10:15:13 -07:00
Leonardo de Moura
051615712c
fix(kernel/quotient/quotient): bug in reduction rule
2015-04-29 10:01:17 -07:00
Leonardo de Moura
d2c7b5c319
feat(library/tactic): add 'let' tactic
...
closes #555
2015-04-28 17:24:43 -07:00
Leonardo de Moura
1be72f1faa
feat(frontends/lean): parse argument of unary tactis with rbp=0, tokens may have a different precedence in expression and tactic modes
2015-04-28 13:43:05 -07:00
Leonardo de Moura
a23118d357
feat(frontends/lean): add tactic_notation command
...
This addresses the first part of issue #461
We still need support for tactic definitions
2015-04-27 17:46:13 -07:00
Leonardo de Moura
ca8943f45b
feat(library,hott): remove rapply tactic
2015-04-27 15:06:16 -07:00
Leonardo de Moura
9d01868361
feat(frontends/lean): use rewrite tactic to implement unfold (it has a unfold step)
...
closes #502
2015-04-24 17:23:12 -07:00
Leonardo de Moura
28404fe16d
fix(library/tactic/rewrite_tactic): second problem reported at issue #548
...
closes #548
2015-04-24 16:49:32 -07:00
Leonardo de Moura
6134c8822a
fix(frontends/lean/util): assertion violation
...
fixes #559
2015-04-24 15:09:23 -07:00
Leonardo de Moura
f723550d33
feat(frontends/lean/elaborator): decorates error message with free variables introduced by the left-hand-side of the equation
...
closes #528
2015-04-24 14:58:15 -07:00
Leonardo de Moura
8241863abe
feat(kernel/hits): add two builtin HITs: type_quotient and trunc
2015-04-23 15:32:31 -07:00
Leonardo de Moura
2613e7c444
fix(frontends/lean): bug when handling identifiers in tactics
...
This bug was reported by Jeremy in the Lean Google group:
https://groups.google.com/forum/?utm_medium=email&utm_source=footer#!msg/lean-discuss/ZKJ8WPPEVJA/n05x6rPRzvMJ
2015-04-22 16:03:22 -07:00
Leonardo de Moura
e1a609cad9
fix(tests/lean/interactive/findp): test output to reflect changes in the stdlib
2015-04-22 13:08:56 -07:00
Leonardo de Moura
349cdb3fe7
test(tests/lean): add test showing that the binder type update should not change the parameter order
2015-04-22 13:04:05 -07:00
Leonardo de Moura
a526cd92ac
fix(frontends/lean): bug in pretty printer
...
this is related to issue #530
2015-04-22 12:44:08 -07:00
Leonardo de Moura
dc93603b4a
feat(frontends/lean): parameter and variable binder type update
...
see issue #532
2015-04-22 12:28:11 -07:00
Leonardo de Moura
91f21c007a
feat(frontends/lean): remove 'context' command
2015-04-22 11:32:02 -07:00
Leonardo de Moura
53653c3526
fix(frontends/lean): pretty printing in sections with parameters
...
fix #530
2015-04-21 22:44:09 -07:00
Leonardo de Moura
8e9997e253
chore(tests/lean/interactive/sec_info_bug): remove 'context' command from test
2015-04-21 19:52:01 -07:00
Leonardo de Moura
fe9f4dd95f
fix(frontends/lean): another bug in sections with parameters
2015-04-21 19:50:21 -07:00
Leonardo de Moura
3df99e514b
fix(frontends/lean): problems with sections
2015-04-21 19:46:57 -07:00
Leonardo de Moura
9fb7aa9f1c
chore(tests): remove most occurrences of 'context' command from the test suite
2015-04-21 19:33:21 -07:00
Leonardo de Moura
ce153d01f9
test(tests/lean/sec_notation2): notation nested in namespace/section/section
2015-04-21 19:07:52 -07:00
Leonardo de Moura
52e9ad1a98
feat(frontends/lean): allow persistent notation declaration in sections (when they do not contain parameters)
...
see issue #554
2015-04-21 19:04:06 -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
697a536d9e
fix(library/tactic/inversion_tactic): type incorrect term being built by 'cases' tactic
...
fixes #545
2015-04-20 19:24:52 -07:00
Leonardo de Moura
107763a506
fix(frontends/lean): better error message for 'proof ... qed' blocks containing unsolved placeholders
2015-04-20 15:50:37 -07:00
Leonardo de Moura
6f6d106a10
feat(library/tactic): add "check_expr" tactic
...
closes #486
2015-04-19 19:00:05 -07:00
Leonardo de Moura
60e320fd79
feat(frontends/lean): protected constants and axioms
...
fixes #527
2015-04-19 17:45:58 -07:00
Leonardo de Moura
b7ca2a0ec9
fix(library/tactic/exact_tactic): exact and or_else
...
fixes #543
2015-04-19 17:23:09 -07:00
Leonardo de Moura
306087b5d3
refactor(library/data): rename 'countable' to 'encodable', define countable in the usual way, and prove all 'encodable' type is 'countable'
2015-04-19 14:20:47 -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
3e5796acb2
fix(tests/lean/abbrev1): to reflect recent changes
2015-04-18 10:40:46 -07:00
Leonardo de Moura
f16eaf8f0f
test(tests/lean/run/pickle1): add unpickle/pickle test
2015-04-14 21:32:07 -07:00
Leonardo de Moura
795acc70a6
refactor(library/data/finset): move finset to its own directory
2015-04-09 19:30:09 -07:00
Leonardo de Moura
4416d9b2c5
test(tests/lean/run): add basic tests for finset module
2015-04-09 15:56:41 -07:00
Leonardo de Moura
24f1454c0a
fix(tests/lean/interactive/findp): adjust test output to reflect recent changes in the pretty printer
2015-04-08 09:49:22 -07:00
Leonardo de Moura
5d95cb0979
feat(library/tactic): add 'refine' tactic
...
closes #482
2015-04-06 18:36:56 -07:00
Leonardo de Moura
412f03b08b
feat(library/tactic/exact_tactic): generate error if 'exact' tactic produces a term containing metavariables
2015-04-06 13:38:53 -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
969d17fd12
fix(frontends/lean/elaborator): class inference in tactic mode with trunc
...
closes #477
2015-04-05 17:47:14 -07:00
Leonardo de Moura
bebe8a4f17
fix(tests/lean/bad_coercions): expected output
2015-04-05 03:00:29 -07:00
Leonardo de Moura
d731a4ab13
feat(library/normalize): add '[unfold-f]' hint
...
closes #497
2015-04-05 03:00:13 -07:00
Leonardo de Moura
d591c63840
feat(frontends/lean/decl_cmds): allow local coercions in contexts
...
closes #525
2015-04-04 15:25:07 -07:00
Leonardo de Moura
8c59f17605
feat(frontends/lean): 'using' expression without 'show' or 'have'
...
closes #536
2015-04-04 15:25:07 -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
1150b19598
perf(frontends/lean/elaborator): do not invoke recursive equation compiler when equations still contain metavariables
2015-04-02 23:37:33 -07:00
Leonardo de Moura
f8023403af
test(tests/lean/run): add another simple test
2015-04-01 15:49:01 -07:00
Leonardo de Moura
bf142f3f18
fix(tests/lean): adjust tests to reflect changes in the standard library
2015-04-01 15:09:00 -07:00
Leonardo de Moura
0d66d19ba3
feat(tests/lean/run/finset): show that if A has decidable equality, then (finset A) also has it.
2015-04-01 13:19:16 -07:00
Leonardo de Moura
b960e123b1
feat(kernel): add experimental support for quotient types
2015-03-31 22:04:16 -07:00
Leonardo de Moura
82833bcbe8
fix(tests/lean/struct_class): add setoid to expected output
2015-03-31 22:03:57 -07:00
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
Leonardo de Moura
fa79b214b8
fix(frontends/lean): allow 'attribute <id> [priority ...]'
2015-03-03 16:17:32 -08:00
Leonardo de Moura
3b73e100dc
test(tests/lean/run): add [priority] test using num.sub
2015-03-03 15:59:17 -08:00
Leonardo de Moura
efd096e85c
feat(library/init/num): define sub and le for binary numerals
2015-03-03 15:55:16 -08:00
Leonardo de Moura
11aad4449b
feat(frontends/lean): add '[semireducible]' attribute
...
This commit also renames the elements of reducible_status.
The idea is to use in the C++ implementation the same names used in the
Lean front-end.
2015-03-03 10:48:36 -08:00
Leonardo de Moura
b254c78c44
refactor(library/algebra): move bundled structures to separate module
...
Motivation: performance.
After this commit, the bundled instances do not participate in the
class/instance resolution if we do not import algebra.bundled.
2015-03-02 18:45:08 -08:00
Leonardo de Moura
8240d7adcd
perf(frontends/lean/util): improve univ_metavars_to_params_fn
...
We moved to replace_visitor because it uses a more precise cache.
2015-03-02 18:25:00 -08:00
Leonardo de Moura
c81762970e
fix(frontends/lean/elaborator): revert commit ededf4fc6c
...
The instantiate_all are needed. See issue #457
2015-03-02 13:00:54 -08:00
Leonardo de Moura
ededf4fc6c
feat(frontends/lean): remove unnecessary instantiate_all's that were messing with error localization
2015-03-01 14:51:44 -08:00
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
dc62bc498f
fix(tests/lean/hott/443_b): adjust test to reflect changes in the HoTT library
2015-02-28 08:46:00 -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
0b48f406f9
fix(tests/lean/hott): adjust tests to reflect changes in the HoTT library
2015-02-26 10:51:19 -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
Leonardo de Moura
383c0d6d4c
fix(tests/lean/interactive/findp): adjust test to reflect recent changes in the standard library
2015-02-25 14:08:37 -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
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
275068641e
fix(tests/lean/print_ax2): adjust test output
2015-02-24 13:34:52 -08:00
Leonardo de Moura
4364b7f926
feat(frontends/lean): pp.beta is true by default
...
Remark: there is one exception (command: print definition). For this
command pp.beta is still false.
2015-02-24 12:27:53 -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
787fed95aa
fix(library/tactic/inversion_tactic): bug in simpler case (hypotheses were being lost)
2015-02-23 16:10:49 -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
923fed8612
fix(frontends/lean/structure_cmd): bug in alias generation in the structure command
...
This commit (and 75acb3bc66
) closes #443
2015-02-23 15:17:05 -08:00
Leonardo de Moura
75acb3bc66
fix(frontends/lean/structure_cmd): internal name of parameter/variable was being erased
2015-02-23 15:01:27 -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
753b9dcd75
fix(tests/lean/hott): adjust tests to reflect changes in standard library
2015-02-22 09:39:27 -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
421a30d75c
feat(library): export [reducible] annotations from function namespace to top-level
...
see issue #433
2015-02-16 18:52:41 -08:00
Leonardo de Moura
7fc216183e
feat(library/tactic): produce better error message when a tactic fails
...
closes #348
2015-02-16 18:42:15 -08:00
Leonardo de Moura
461c02d790
fix(tests/lean/hott/433): remove bogus comment, and use rewrite tactic
...
Fix an issue raised by Floris.
See discussion at
https://github.com/leanprover/lean/issues/433
2015-02-16 15:45:31 -08:00
Leonardo de Moura
4248ad644d
fix(frontends/lean): priority expressions parser
2015-02-14 12:26:06 -08:00
Leonardo de Moura
5cbdd77ad0
feat(library/tactic/rewrite_tactic): improve matcher in rewrite_tactic
...
closes #433
2015-02-13 12:40:55 -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
04e92e1e96
feat(frontends/lean/parser): reject explicit universe levels in variables and parameters
...
This modification was motivated by issue #427
2015-02-11 16:25:06 -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
eceed03044
feat(frontends/lean): add "except" notation for "open" command, allow multiple metaclasses to be opened in a single "open" command
2015-02-11 11:02:59 -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
60fca7575c
fix(frontends/lean/pp): bugs when pretty printing abbreviations
2015-02-10 19:06:09 -08:00
Leonardo de Moura
f9832fb89f
test(tests/lean/abbrev1): add test for abbreviation command
2015-02-10 18:28:48 -08:00
Leonardo de Moura
014271da8b
feat(frontends/lean): better error messages for ill-terminated declarations
2015-02-10 14:38:00 -08:00
Leonardo de Moura
f018fdabb9
refactor(library/kernel_bindings): remove unnecessary procedure
2015-02-07 18:57:46 -08:00
Leonardo de Moura
c04c0e8381
refactor(*): remove transparent_scope hack, replace [strict] with [all-transparent] annotation
2015-02-07 15:19:41 -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
90eb5c8ca5
test(tests/lean/hott): add test for rewriter in the HoTT version
2015-02-04 19:33:08 -08:00
Leonardo de Moura
61a029d9df
fix(tests/lean/rewrite_loop): notation
2015-02-04 19:21:26 -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
89fde9d829
feat(library/tactic/rewrite_tactic): add maximum number of iterations threshold to rewrite tactic
...
The idea is to avoid nontermination.
2015-02-04 16:13:15 -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
2a6ccb252e
test(tests/lean/extra): add regression tests for issue #422
2015-02-04 10:55:03 -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
10357f3f53
fix(tests/lean/nonexhaustive): remove line "warning: imported file uses 'sorry'" from test produced output
2015-02-01 21:25:52 -08:00
Leonardo de Moura
36cfb7fac0
test(tests/lean/bad_set_option): add tests for bad 'set_option' command
2015-02-01 20:20:35 -08:00
Leonardo de Moura
9d1e312c12
test(tests/lean/extra): add extra tests for 'print' command
2015-02-01 20:20:26 -08:00
Leonardo de Moura
ed85ac254a
test(tests/lean): add more tests for error messages
2015-02-01 20:04:22 -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
7d9d89bae6
test(tests/lean/extra): add test for saving recursive equation pre-terms
2015-02-01 19:49:14 -08:00
Leonardo de Moura
2403d555ee
test(tests/lean/bad_eqns): add tests for definition package error messages
2015-02-01 19:36:06 -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
Leonardo de Moura
ea9a9d63d1
test(tests/lean): add tests for structure command error messages
2015-01-30 09:52:42 -08:00
Leonardo de Moura
7c59c959db
fix(tests/lean/interactive): do not compare output of trace using non-deterministic commands such as "WAIT ms"
2015-01-30 09:52:42 -08:00
Leonardo de Moura
e75828b756
test(tests/lean/interactive): add tests for options structure.eta_thm and structure.proj_mk_thm
2015-01-29 16:52:23 -08:00
Leonardo de Moura
e9d8a960d9
test(tests/lean/interactive): add test for proof_state info
2015-01-29 16:44:10 -08:00
Leonardo de Moura
c74da8bea2
test(tests/lean/interactive): add tests for coercion and overload info
2015-01-29 16:39:27 -08:00
Leonardo de Moura
f04e462bf3
test(tests/lean/interactive): add more tests for lean server
2015-01-29 16:30:07 -08:00
Leonardo de Moura
e9e1f86b7f
fix(library/app_builder): many bugs, add use_cache option, add tests
2015-01-29 15:30:31 -08:00
Leonardo de Moura
5bb2a41c64
feat(library/reducible): expose Lua API for reducible hints
2015-01-29 10:37:15 -08:00
Leonardo de Moura
e4b5e07498
fix(frontends/lean/elaborator): apply substitution before compiling pre-tactics into tactics
...
closes #415
2015-01-28 13:32:56 -08:00
Leonardo de Moura
94519b48b1
fix(tests/lean): adjust tests to reflect changes in the standard library
2015-01-27 11:37:17 -08:00
Leonardo de Moura
ad4c7c20f9
fix(kernel/inductive/inductive): fix assertion violation when K is applied to type incorrect term
2015-01-27 11:22:14 -08:00
Leonardo de Moura
e2c41fca75
feat(frontends/lean): modify syntax for local notation
...
The idea is to make it uniform with the syntax for defining local
attributes.
2015-01-26 11:51:17 -08:00
Leonardo de Moura
b4d6f6e3ed
feat(frontends/lean): 'attribute' command is persistent by default
2015-01-26 11:51:17 -08:00
Leonardo de Moura
a1eeb0a6a1
fix(library/print): typo in is_used_name
...
closes #408
2015-01-25 08:58:08 -08:00
Leonardo de Moura
4f2e0c6d7f
refactor(frontends/lean): add 'attribute' command
...
The new command provides a uniform way to set declaration attributes.
It replaces the commands: class, instance, coercion, multiple_instances,
reducible, irreducible
2015-01-24 20:23:21 -08:00
Leonardo de Moura
b5c4e603db
feat(frontends/lean): allow parameters to be used in sections
...
Restriction:
- coercions and notations cannot be defined in parametric sections
closes #401
2015-01-23 17:42:19 -08:00
Leonardo de Moura
42b5b1e679
test(tests/lean): add new test for scoping rules
2015-01-22 11:41:19 -08:00
Leonardo de Moura
880faf89e0
feat(frontends/lean/structure_cmd): add implicit_infer_kind annotation to structure command
...
closes #354
2015-01-21 18:12:29 -08:00
Leonardo de Moura
12674114a4
feat(shell): set default behavior to "trusted"
...
closes #402
2015-01-21 16:25:09 -08:00
Leonardo de Moura
f2e878dbe7
fix(tests/lua/res1): adjust test to recent modifications
2015-01-20 16:26:41 -08:00
Leonardo de Moura
260795f981
fix(frontends/lean/structure_cmd): collect universe levels that only occur in structure parameters
...
fixes #395
2015-01-19 22:18:09 -08:00
Leonardo de Moura
002050fa97
feat(frontends/lean): increase binding power of ! and @
...
Remark: I did not add the constant "app".
Reason: It would break the standard library in many places.
Moreover, the current "max" is not just the binding power of
application, but also the binding power of identifiers, (, [, ...
It would be weird to call it "app"
closes #388
2015-01-19 18:40:33 -08:00
Leonardo de Moura
6fd0d452d3
test(tests/lean/run): adjust tests to reflect recent changes
2015-01-19 18:00:14 -08:00
Leonardo de Moura
edcc92d9c7
feat(frontends/lean): remove 'using' from structure instance command
2015-01-17 09:38:10 -08:00
Leonardo de Moura
fed96c9e0b
test(tests/lean/run): add structure instance example
2015-01-17 09:27:15 -08:00
Leonardo de Moura
f9d7480f5c
feat(frontends/lean): notation for creating structure instances
2015-01-16 17:14:30 -08:00
Leonardo de Moura
bfd679d52d
feat(frontends/lean/structure_cmd): allow user to reference parent structures when defining new fields
...
See new test for an example.
closes #371
2015-01-16 13:04:48 -08:00
Leonardo de Moura
6c07ca5d41
perf(library/print): improve is_used_name
2015-01-15 19:01:13 -08:00