Leonardo de Moura
64c3927e0b
feat(library/equations_compiler/elim_match): report unused equations
...
closes #1162
2016-10-19 09:58:08 -07:00
Leonardo de Moura
e74cfa9db7
fix(library/equations_compiler/elim_match): bug at complete transition
...
It also updates the condition for triggering the inaccessible
transition. Before this commit, we would only perform this kind
of transition if *all* terms were marked inaccessible. Now,
we perform it if *some* are marked inaccessible. Reason:
when we perform the complete transition we don't have enought
information for deciding whether an argument should be marked as
inaccessible or not. If this decision creates confusion for users,
we may try to mark them with an "maybe-inaccessible" annotation, and
then enforce that the inaccessible transition is performed onlty if
*all* terms are marked as inaccessible or *maybe-inaccessible"
2016-10-19 09:10:19 -07:00
Leonardo de Moura
7b806755d9
chore(library/tactic/simplify): remove subsingleton support
...
It is left over from the blast tactic.
Moreover, it is incomplete.
2016-10-16 22:11:12 -07:00
Leonardo de Moura
9810a5f941
refactor(library/tactic/simplifier): simplify simplifier
2016-10-16 15:55:30 -07:00
Leonardo de Moura
0f72de217a
chore(library/tactic/simplifier): simplify simplifier
2016-10-15 18:14:59 -07:00
Leonardo de Moura
bf7bae6eaf
feat(library/init/meta/tactic): add beta/zeta tactics
2016-10-13 18:47:27 -07:00
Daniel Selsam
b4644acba4
fix(meta/mk_dec_eq_instance): handle indices and ginductives
2016-10-13 10:12:37 -07:00
Leonardo de Moura
ef23c591fc
feat(library/init/meta): implement unfold tactics in Lean using new building blocks
2016-10-12 17:25:56 -07:00
Leonardo de Moura
4f2db5702f
feat(library/tactic/unfold_tactic): allow user to set transparency_mode at dunfold_expr
2016-10-12 14:07:50 -07:00
Leonardo de Moura
46eb7decde
feat(library/tactic/unfold_tactic): add unfold_projection tactic
2016-10-12 13:43:32 -07:00
Leonardo de Moura
deb2bb92b2
feat(library/tactic/simp_lemmas_tactics): add dunfold_expr tactic based on equational lemmas
2016-10-12 13:18:10 -07:00
Leonardo de Moura
f66aec2309
feat(library/tactic/simp_lemmas_tactics): add simp_lemmas.drewrite
2016-10-12 09:01:47 -07:00
Leonardo de Moura
1a4ac3a102
fix(library/tactic/dsimplify): bugs and implement dsimp using new dsimplify
2016-10-12 08:33:40 -07:00
Leonardo de Moura
e37207e8a9
feat(library/tactic): expose new dsimplify in Lean
2016-10-12 07:25:09 -07:00
Leonardo de Moura
d655310ecf
feat(library/init/meta): rename rsimp* back to dsimp*
2016-10-11 16:37:08 -07:00
Leonardo de Moura
231c124be8
feat(library/init/meta): rename dsimp => rsimp, and add primitive tactic that takes an arbitrary simp_lemmas
2016-10-09 10:02:26 -07:00
Leonardo de Moura
a78e8fb11a
refactor(library/tactic/simp_lemmas_tactics): consistent naming
2016-10-09 09:37:20 -07:00
Daniel Selsam
1644e52c47
fix(frontends/lean/decl_cmds): allow noncomputable meta
2016-10-08 22:21:56 -07:00
Leonardo de Moura
476684a284
refactor(library,library/tactic/defeq_simplifier): use simp_lemmas in the defeq_simplifier
2016-10-08 22:15:27 -07:00
Leonardo de Moura
eaef8dae20
chore(library/init/core): remove unnecessary annotations
2016-10-07 16:09:14 -07:00
Leonardo de Moura
3fbdb71f3e
feat(library/tactic/simplifier): remove simp_extensions
2016-10-06 20:50:23 -07:00
Leonardo de Moura
d747fcb17c
refactor(library/tactic/simp_lemmas): new caching mechanism
2016-10-06 20:20:01 -07:00
Leonardo de Moura
91076b06ad
feat(library/init/meta/converter): add 'find_pattern' conversional
2016-10-05 19:22:17 -07:00
Leonardo de Moura
895a94d17e
feat(library/init/meta/converter): match based conversions
2016-10-05 18:54:11 -07:00
Leonardo de Moura
68df31df67
feat(library/init/meta/converter): add adapter for applying propext automatically
2016-10-05 17:13:28 -07:00
Leonardo de Moura
990c414b86
feat(library/init/meta/converter): add 'congr' and 'depthfirst' conversionals
2016-10-05 15:05:22 -07:00
Leonardo de Moura
a6808cfbad
fix(library/init/meta/converter): fix conversion error message
2016-10-05 15:05:22 -07:00
Leonardo de Moura
4a9a637ddf
feat(library/init/meta/converter): add 'funext' converter and 'conversion' tactic
2016-10-05 15:05:07 -07:00
Leonardo de Moura
3a3e30523b
feat(library/init/meta): start converter library
2016-10-04 20:50:54 -07:00
Leonardo de Moura
6b582ca6c3
fix(library/vm/vm): bug at get_constant
2016-10-04 01:58:39 -07:00
Leonardo de Moura
269fb198fb
perf(library/type_context): process function before arguments
2016-10-03 23:34:14 -07:00
Leonardo de Moura
629cfa6ba1
feat(library/tactic/simplifier): disable broken theory_simplifiers
2016-10-03 22:06:44 -07:00
Leonardo de Moura
f9ca306fe2
chore(tests/lean/run): fix tests
2016-10-03 21:44:48 -07:00
Leonardo de Moura
d549044d27
feat(library/init/meta,library/tactic/simplifier): user defined simp attributes
2016-10-03 21:39:17 -07:00
Leonardo de Moura
4a2946f5dd
feat(library/tactic/eval): eval_expr for arbitrary expressions
2016-10-03 19:01:22 -07:00
Leonardo de Moura
7465529445
feat(library/tactic): 'eval_expr' tactic skeleton
2016-10-03 16:26:28 -07:00
Leonardo de Moura
838b3329ce
fix(frontends/lean/elaborator): structure instance update with type classes
2016-10-02 11:36:22 -07:00
Leonardo de Moura
f21f1219d9
fix(frontends/lean/structure_cmd): handle is_one_placeholder
2016-10-02 08:07:19 -07:00
Leonardo de Moura
f73506256c
chore(tests/lean): adjust tests
2016-10-01 12:57:56 -07:00
Leonardo de Moura
8730def4f9
feat(library/init): add basic algebra
2016-09-30 20:51:22 -07:00
Leonardo de Moura
c0022253a7
feat(frontends/lean/tactic_notation): allow lemmas to be removed
2016-09-30 19:53:51 -07:00
Leonardo de Moura
fd6dc8154a
feat(library/init/meta/interactive): add interactive tactics
2016-09-30 19:02:45 -07:00
Leonardo de Moura
d627011786
feat(frontends/lean/tactic_notation): do is tactic unit in begin end blocks.
2016-09-30 16:35:45 -07:00
Leonardo de Moura
051b6bd026
feat(frontends/lean/tactic_notation): add notation for entering auto-quotation mode
2016-09-30 16:18:52 -07:00
Leonardo de Moura
9ea858e6fe
feat(frontends/lean/tactic_notation): nested interactive tactics
2016-09-30 14:53:07 -07:00
Leonardo de Moura
23ce2b0587
feat(frontends/lean/tactic_notation, library/init/meta/interactive): add "interactive" versions of define/assert/definev/assertv/note tactics
2016-09-29 18:48:32 -07:00
Leonardo de Moura
572751c56e
feat(frontends/lean): force user to use meta keyword on meta inductive/structure/class
...
Before this commit, we were inferring whether an
inductive/structure/class were meta or not. This was bad since the user
had no clue whether the type was trusted (non meta) or not.
Moreover, users could get confused by this behavior and assume the
kernel was allowing trusted code to rely on untrusted one.
2016-09-29 17:56:35 -07:00
Leonardo de Moura
c8a720212b
feat(frontends/lean): 'by' is now also using interactive mode syntax
2016-09-29 01:57:40 -07:00
Leonardo de Moura
84b45b010a
feat(frontends/lean/elaborator): improve overloading support
2016-09-28 20:54:11 -07:00
Leonardo de Moura
92373bb749
feat(library/type_context): universe constraint postponement
2016-09-28 15:30:14 -07:00
