Leonardo de Moura
|
195512e125
|
fix(library/type_context, library/tactic/revert_tactic): result must contain also reverted let-decls
|
2016-06-21 16:32:02 -07:00 |
|
Leonardo de Moura
|
359b566088
|
feat(library/tactic/subst_tactic): add tracing for subst tactic
|
2016-06-21 16:31:53 -07:00 |
|
Leonardo de Moura
|
6fa6554b4d
|
fix(library/tactic/intro_tactic): fix 'intron' tactic
|
2016-06-21 16:30:26 -07:00 |
|
Leonardo de Moura
|
2a2d7530b2
|
fix(library/tactic/intro_tactic): typo
|
2016-06-21 16:14:28 -07:00 |
|
Leonardo de Moura
|
fd08a9badf
|
refactor(library/local_context): store pp_name in local_ref's
This commit also removes the now obsolete API get_local_pp_name from abstract_type_context
|
2016-06-21 10:50:38 -07:00 |
|
Leonardo de Moura
|
16c050b66c
|
reactor(library): port fun_info_manager to new type_context (and rename module to fun_info)
|
2016-06-21 10:42:38 -07:00 |
|
Leonardo de Moura
|
d912c31f60
|
feat(library/tactic/app_builder_tactics): add transparency param to mk_app and mk_mapp tactics
|
2016-06-21 09:55:18 -07:00 |
|
Leonardo de Moura
|
9321f83267
|
feat(library/type_context): new scopes for entering tmp_mode
|
2016-06-21 09:48:28 -07:00 |
|
Leonardo de Moura
|
d03dc18096
|
chore(library/tactic/tactic_state): add helper methods
|
2016-06-20 10:47:48 -07:00 |
|
Leonardo de Moura
|
851bc30f3a
|
fix(library/type_context): make sure explicitly reverted locals occur first
|
2016-06-20 10:45:26 -07:00 |
|
Leonardo de Moura
|
6e007cd12f
|
fix(library/app_builder): use current context when tracing
|
2016-06-20 10:29:43 -07:00 |
|
Leonardo de Moura
|
397ea25e24
|
fix(library/tactic/subst_tactic): use intermediate state for errors
|
2016-06-20 10:22:36 -07:00 |
|
Leonardo de Moura
|
32f382991a
|
feat(library/init/meta/tactic): intro returns new free_var
|
2016-06-20 09:37:06 -07:00 |
|
Leonardo de Moura
|
a2745aa273
|
perf(library/metavar_util): do nothing if term does not contain assigned metavars
|
2016-06-20 09:06:04 -07:00 |
|
Leonardo de Moura
|
02904c5b87
|
feat(library/init/meta): add 'reflexivity', 'symmetry' and 'transitivity' tactics
|
2016-06-18 20:01:53 -07:00 |
|
Leonardo de Moura
|
05eafa08eb
|
chore(library/tactic/tactic_state): style
|
2016-06-18 14:55:47 -07:00 |
|
Leonardo de Moura
|
90d07a7360
|
feat(library/tactic/clear_tactic): add 'clear_fv' tactic
|
2016-06-18 14:43:57 -07:00 |
|
Leonardo de Moura
|
dc180dcd15
|
feat(library/tactic/assert_tactic): add 'pose' tactic
|
2016-06-18 14:28:28 -07:00 |
|
Leonardo de Moura
|
b546167a64
|
feat(library/tactic/tactic_state): add tactic mk_fresh_name
|
2016-06-18 13:02:45 -07:00 |
|
Leonardo de Moura
|
5021b02043
|
feat(library/init/meta/tactic,library/tactic/tactic_state): add tactics for setting options
|
2016-06-18 12:05:58 -07:00 |
|
Leonardo de Moura
|
5846dc1812
|
feat(library/tactic/tactic_state): add get_assignment and get_univ_assignment
|
2016-06-18 11:34:00 -07:00 |
|
Leonardo de Moura
|
6a0f11f705
|
feat(library/tactic/tactic_state,library/init/meta/tactic): add mk_meta_univ, mk_meta_var, mk_const
This commit also changes the semantics of the unify tactic.
It fails if the arguments are not unifiable.
|
2016-06-18 11:12:51 -07:00 |
|
Leonardo de Moura
|
f05e0cfa5a
|
fix(library/tactic/apply_tactic): instantiate metavariables before type class resolution
|
2016-06-18 10:38:54 -07:00 |
|
Leonardo de Moura
|
9cc3fb90ff
|
chore(library/tactic/apply_tactic): remove trace msg
|
2016-06-18 10:35:12 -07:00 |
|
Leonardo de Moura
|
00717318f0
|
feat(library/tactic/apply_tactic): add option to disable type class resolution to apply_core
|
2016-06-18 10:03:38 -07:00 |
|
Leonardo de Moura
|
735aa4ebfa
|
feat(library/tactic/tactic_state): add 'is_class' and 'apply_instance' tactics
|
2016-06-18 09:51:02 -07:00 |
|
Leonardo de Moura
|
66c6d3b87a
|
feat(library/tactic/apply_tactic): add remove_redundant_goals
|
2016-06-17 20:21:17 -07:00 |
|
Leonardo de Moura
|
61a845c005
|
feat(library/tactic): add 'apply' tactic
|
2016-06-17 20:11:52 -07:00 |
|
Leonardo de Moura
|
ded1fe74c5
|
refactor(library/init/meta/tactic): implement num_goals in Lean
|
2016-06-17 16:18:15 -07:00 |
|
Leonardo de Moura
|
b21a3376e0
|
feat(library/init/meta/tactic): add 'focus' and 'all_goals' tacticals
|
2016-06-17 16:11:40 -07:00 |
|
Leonardo de Moura
|
6371a8db38
|
fix(library/tactic/tactic_state): consume solved goals
|
2016-06-17 15:19:50 -07:00 |
|
Leonardo de Moura
|
0b2ed21561
|
feat(library/init/meta/tactic): add rotate_left and rotate_right tactics
|
2016-06-17 15:11:08 -07:00 |
|
Leonardo de Moura
|
eef3debcf5
|
fix(library/type_context): bug in revert with let-decls
|
2016-06-17 14:50:01 -07:00 |
|
Leonardo de Moura
|
c5f92f08b8
|
feat(library/tactic): add 'assert' tactic
Remark: the new assert tactic does have the problem described in issue #621
|
2016-06-17 14:42:28 -07:00 |
|
Leonardo de Moura
|
87a5b88f66
|
fix(library/type_context): typo
|
2016-06-17 13:57:50 -07:00 |
|
Leonardo de Moura
|
d0afe0aa99
|
feat(library/tactic): add 'change' tactic
|
2016-06-17 13:21:52 -07:00 |
|
Leonardo de Moura
|
73b21b9e48
|
fix(library): assertion violations
|
2016-06-17 13:16:17 -07:00 |
|
Leonardo de Moura
|
e53ce1828a
|
fix(library/defeq_simplifier): assertion
|
2016-06-17 12:30:09 -07:00 |
|
Leonardo de Moura
|
2d6742b091
|
feat(library/tactic): add tactic.defeq_simp
|
2016-06-17 11:20:15 -07:00 |
|
Leonardo de Moura
|
f36db4085e
|
feat(library/trace): add helper constructor
|
2016-06-17 11:17:08 -07:00 |
|
Leonardo de Moura
|
1fb8cc0dfd
|
feat(library/defeq_simplifier): move defeq simplifier to new type_context
|
2016-06-17 10:51:07 -07:00 |
|
Leonardo de Moura
|
8333500457
|
refactor(library): move try_eta to util
|
2016-06-17 10:29:02 -07:00 |
|
Leonardo de Moura
|
c8c43a866b
|
feat(library/tactic): implement assumption tactic in Lean
|
2016-06-17 09:06:35 -07:00 |
|
Leonardo de Moura
|
27085c3d16
|
feat(library/tactic/tactic_state): add tactic.mk_instance
|
2016-06-17 08:39:18 -07:00 |
|
Leonardo de Moura
|
7f03684d89
|
fix(library/tactic/tactic_state): forgot to register tactic.whnf
|
2016-06-16 18:23:57 -07:00 |
|
Leonardo de Moura
|
586baa4118
|
feat(library,frontends/lean): support for quoted expressions in the VM, compiler and frontend
TODO: invoke elaborator at tactic.to_expr
|
2016-06-15 16:06:39 -07:00 |
|
Leonardo de Moura
|
5b8ac6ba30
|
feat(library/tactic): add 'exact' tactic
|
2016-06-14 21:30:58 -07:00 |
|
Leonardo de Moura
|
cb9b5650b7
|
feat(library/tactic): add 'subst' tactic
|
2016-06-14 21:01:57 -07:00 |
|
Leonardo de Moura
|
a136c2ec1e
|
fix(library/tactic/revert_tactic): update output parameter
|
2016-06-14 17:56:12 -07:00 |
|
Leonardo de Moura
|
50b6f9517a
|
feat(library/tactic/app_builder_tactics): add tactic.mk_mapp
|
2016-06-14 17:33:32 -07:00 |
|