Leonardo de Moura
|
a544d32fcf
|
fix(frontends/lean/elaborator): missing information when displaying unsolved placeholders
|
2014-10-26 16:11:58 -07:00 |
|
Leonardo de Moura
|
cc6a96e8ba
|
fix(frontends/lean): improve begin-end construct
|
2014-10-26 15:47:29 -07:00 |
|
Leonardo de Moura
|
fd60cf6a79
|
feat(library/tactic/exact_tactic): modify 'exact' tactic semantics, use higher-order unification
See new node.inj4 theorem, we need the extra power to be able to avoid type information at
exact (assume e₁ e₂, e₁)
|
2014-10-26 10:27:33 -07:00 |
|
Leonardo de Moura
|
8e6de93394
|
fix(frontends/lean/parser): add two kinds of no_undef_id behavior: to (global) constant; to local constant
|
2014-10-26 09:47:11 -07:00 |
|
Leonardo de Moura
|
c7f6a6b94e
|
feat(library/definitional/cases_on): automatically add 'cases_on'
|
2014-10-25 17:22:02 -07:00 |
|
Leonardo de Moura
|
cdcde661ef
|
feat(library/definitional/induction_on): automatically add 'induction_on'
|
2014-10-25 13:37:04 -07:00 |
|
Leonardo de Moura
|
a7a06ab0f8
|
feat(library/definitional/rec_on): automatically generate rec_on function for inductive datatypes
|
2014-10-25 13:08:59 -07:00 |
|
Leonardo de Moura
|
7a033ac07e
|
feat(frontends/lean): add 'print axioms' command, close #251
|
2014-10-24 14:35:03 -07:00 |
|
Leonardo de Moura
|
db25f933b0
|
feat(frontends/lean): use nice names for meta-variables when executing check c and c is a constant
|
2014-10-24 08:23:26 -07:00 |
|
Leonardo de Moura
|
79d0347721
|
feat(library/tactic): add generalize tactic, closes #34
Remark: the intros tactic has been added in a different commit: 7d0100a340
|
2014-10-23 22:40:15 -07:00 |
|
Leonardo de Moura
|
b83b065d00
|
feat(library/tactic/apply_tactic): modify heuristic for adding arguments to apply tactic.
|
2014-10-23 22:36:32 -07:00 |
|
Leonardo de Moura
|
f027acb5cb
|
fix(frontends/lean): missing type info in expressions nested in tactics
|
2014-10-23 18:31:05 -07:00 |
|
Leonardo de Moura
|
212ae0b61c
|
feat(frontends/lean): automatically add 'info' tactic in begin-end blocks
Actually, the tactic is only added when Lean is in collect-info mode.
|
2014-10-23 13:30:04 -07:00 |
|
Leonardo de Moura
|
e750c9b67a
|
feat(frontends/lean): add 'info' tactic for producing PROOF_STATE info for emacs mode
|
2014-10-23 13:18:30 -07:00 |
|
Leonardo de Moura
|
38a9aa2a98
|
feat(frontends/lean): automatically open 'tactic' namespace (if it is not already open) in 'by' and 'begin-end' expressions
|
2014-10-23 10:26:19 -07:00 |
|
Leonardo de Moura
|
00f9a10e82
|
refactor(library/tactic/unfold_tactic): use new 'tactic.expr' to implement 'unfold' tactic
This change also enabled us to remove hacks used in the tests modified
by this commit.
|
2014-10-23 10:26:19 -07:00 |
|
Leonardo de Moura
|
5a553603d1
|
fix(library/general_notation): mark \tr as left associative
|
2014-10-22 22:18:40 -07:00 |
|
Leonardo de Moura
|
c50227ea6e
|
feat(library/tactic): change apply tactic semantics: goals are not reversed; and dependent arguments are not included
This commit also adds the tactic rapply that corresponds to the previous
semantics we have been using.
|
2014-10-22 18:11:09 -07:00 |
|
Leonardo de Moura
|
e95c7c5f70
|
refactor(library/tactic/rename_tactic): use new 'tactic.expr' to implement 'intro/intros' tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-10-22 17:29:50 -07:00 |
|
Leonardo de Moura
|
5e15ac0c92
|
feat(library/tactic): add new approach for embedding non-elaborated expressions into tactics
|
2014-10-22 17:29:50 -07:00 |
|
Leonardo de Moura
|
33f18b9454
|
fix(kernel/converter): remove buggy eta-reduction and rely only on eta-expansion
The bug is exposed by new unit test
|
2014-10-21 16:54:25 -07:00 |
|
Leonardo de Moura
|
6b89080b1a
|
feat(frontends/lean): do not allow user to define notation using tokens ! and @, closes #248
|
2014-10-21 16:28:36 -07:00 |
|
Leonardo de Moura
|
e24225fabf
|
feat(frontends/lean): validate infixl/infixr/postfix/prefix declarations against reserved notations
|
2014-10-21 15:39:47 -07:00 |
|
Leonardo de Moura
|
6c7e23ecaa
|
refactor(library): use 'reserve' notation in the standard library
|
2014-10-21 15:39:47 -07:00 |
|
Leonardo de Moura
|
bb953b80aa
|
feat(frontends/lean): reserve notation, closes #95
|
2014-10-21 15:39:47 -07:00 |
|
Leonardo de Moura
|
8a44dfc1df
|
fix(frontends/lean/pp): bug in pretty printer notation match procedure
|
2014-10-20 18:58:27 -07:00 |
|
Leonardo de Moura
|
40fb66bf07
|
feat(frontends/lean): change default precedence to 1
|
2014-10-20 18:40:55 -07:00 |
|
Leonardo de Moura
|
e2fa981e89
|
fix(frontends/lean/pp): avoid parentheses around atomic notation
|
2014-10-20 18:08:13 -07:00 |
|
Leonardo de Moura
|
e68007a727
|
fix(frontends/lean/builtin_tactics): adjust tactics precedence
|
2014-10-20 17:10:16 -07:00 |
|
Leonardo de Moura
|
9b8f60b739
|
feat(frontends/lean/builtin_exprs): tolerate dangling ',' in begin-end block
This is useful when debugging proofs.
|
2014-10-20 15:59:49 -07:00 |
|
Leonardo de Moura
|
c09bb3cc6f
|
fix(tests/lean/notation): remove 'sorry' warning from expected outputs
|
2014-10-20 15:34:44 -07:00 |
|
Leonardo de Moura
|
7d0100a340
|
feat(library/tactic): add 'intros' tactic
|
2014-10-20 15:26:16 -07:00 |
|
Leonardo de Moura
|
f0cc17af87
|
fix(frontends/lean/elaborator): missing type information when ! operator (aka consume_args) is used
|
2014-10-20 08:31:36 -07:00 |
|
Leonardo de Moura
|
a1006073d4
|
feat(frontends/lean/notation_cmd): do not allow user to define new tokes containing '(', ')', ',' or change their precedence
|
2014-10-19 13:39:06 -07:00 |
|
Leonardo de Moura
|
4d4bc0551f
|
feat(frontends/lean/pp): minimize number of spaces when pretty printing notation
|
2014-10-19 13:08:15 -07:00 |
|
Leonardo de Moura
|
ed1afe26bd
|
feat(frontends/lean/pp): support scopedexpr notation in the pretty printer
|
2014-10-19 12:50:40 -07:00 |
|
Leonardo de Moura
|
f63d47fef3
|
feat(frontends/lean/pp): support foldl/foldr notation in the pretty printer
|
2014-10-19 11:16:24 -07:00 |
|
Leonardo de Moura
|
eef1cc4ac2
|
fix(frontends/lean/pp): implicit arguments in notation
|
2014-10-19 09:04:43 -07:00 |
|
Leonardo de Moura
|
555d26aa61
|
feat(frontends/lean/pp): take notation declarations into account when pretty printing
TODO: support foldl/foldr and binders
|
2014-10-19 08:41:29 -07:00 |
|
Leonardo de Moura
|
28128e0330
|
fix(frontends/lean): EXTRA_TYPE info
|
2014-10-16 12:25:18 -07:00 |
|
Leonardo de Moura
|
e6606ef2ac
|
feat(library/tactic): add 'rename' hypothesis tactic
|
2014-10-14 18:19:34 -07:00 |
|
Leonardo de Moura
|
90dba868e3
|
feat(library/tactic/proof_state): apply substitutions when pretty printing state
|
2014-10-14 17:37:20 -07:00 |
|
Leonardo de Moura
|
58c9421bab
|
refactor(library/tactic): elaborate expressions nested in tactics with respect to current goal, save postponed constraints (e.g., flex-flex constraints) closes #44, fixes #70
|
2014-10-14 17:18:40 -07:00 |
|
Leonardo de Moura
|
d75a9c840c
|
fix(frontends/lean/parser): segfault when ending scope without opening, fixes #244
|
2014-10-13 21:08:36 -07:00 |
|
Leonardo de Moura
|
b7c1b348d1
|
feat(frontends/lean/inductive_cmd): don't force user to repeat argument declarations in every datatype in a mutually recursive datatype declaration
|
2014-10-13 20:53:09 -07:00 |
|
Leonardo de Moura
|
08c0fb3a64
|
test(tests/lean/run): expand tree example
|
2014-10-13 07:08:29 -07:00 |
|
Leonardo de Moura
|
5c1d5133dd
|
fix(library/data/prod): make the notation for tuples and product types consistent
|
2014-10-13 06:48:37 -07:00 |
|
Leonardo de Moura
|
a26618e0f2
|
feat(frontends/lean): add '[]' notation for marking arguments where class-instance resolution should be applied
|
2014-10-12 13:06:00 -07:00 |
|
Leonardo de Moura
|
549f24335e
|
feat(frontends/lean): do not allow coercion definition in sections
|
2014-10-11 18:41:17 -07:00 |
|
Leonardo de Moura
|
158682219f
|
feat(frontends/lean): allow parameters only in contexts
|
2014-10-11 17:13:56 -07:00 |
|