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
Leonardo de Moura
3a3c43f381
refactor(library/init): move unification_hint structure to init folder
2016-09-28 09:35:19 -07:00
Leonardo de Moura
0ba92e4885
feat(tests/lean/run/dep_coe_to_fn3): another dep fn coe test
2016-09-28 09:34:51 -07:00
Leonardo de Moura
d59410cc41
refactor(kernel): support only proof irrelevant mode
2016-09-27 17:18:52 -07:00
Leonardo de Moura
1d83939cc8
test(tests/lean/run): add more tests for coercion to function
2016-09-27 16:10:50 -07:00
Leonardo de Moura
d7c3fce8a3
feat(library/init/coe,frontends/lean): more general coercions to fun
...
The new test dep_coe_to_fn.lean motivates the change.
2016-09-27 15:41:06 -07:00
Gabriel Ebner
d0ab6065c3
fix(frontends/lean): type check examples
2016-09-27 14:39:55 -07:00
Leonardo de Moura
c6ec659bf5
feat(frontends/lean): improve 'begin...end' blocks
2016-09-27 13:34:11 -07:00
