michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
lean2/src/library/tactic
History
Leonardo de Moura 9516cd9ee3 feat(library/tactic): 'exact' tactic report unsolved placeholders in nested expression 
Actually, the elaborator is the one reporting the unassigned
placeholders. The 'exact' tactic just makes the request.
To implement this feature we had to extend the elaboration interface
expected by the tactic framework.
2014-11-28 14:59:35 -08:00
..
apply_tactic.cpp feat(library/tactic): 'exact' tactic report unsolved placeholders in nested expression 2014-11-28 14:59:35 -08:00
apply_tactic.h fix(library/tactic): add relax_main_opaque flag to proof_state objects, closes #274 2014-10-29 08:57:34 -07:00
clear_tactic.cpp refactor(library/tactic): cleanup 'revert' and 'clear' tactics 2014-11-26 17:08:14 -08:00
clear_tactic.h feat(library/tactic): add 'clear' tactic, closes #341 2014-11-26 13:11:36 -08:00
CMakeLists.txt feat(library/tactic): add first step of 'inversion' tactic 2014-11-26 21:28:00 -08:00
elaborate.cpp feat(library/tactic): 'exact' tactic report unsolved placeholders in nested expression 2014-11-28 14:59:35 -08:00
elaborate.h feat(library/tactic): 'exact' tactic report unsolved placeholders in nested expression 2014-11-28 14:59:35 -08:00
exact_tactic.cpp feat(library/tactic): 'exact' tactic report unsolved placeholders in nested expression 2014-11-28 14:59:35 -08:00
exact_tactic.h refactor(library/tactic): move 'exact' tactic to separate module 2014-10-22 17:29:44 -07:00
expr_to_tactic.cpp chore(library/tactic/expr_to_tactic): fix compilation warning 2014-10-29 19:47:47 -07:00
expr_to_tactic.h feat(library/tactic): add rotate_left/rotate_right tactics, closes #278 2014-10-29 19:13:55 -07:00
generalize_tactic.cpp feat(library/tactic): add 'clears' and 'reverts' variants 2014-11-26 14:49:48 -08:00
generalize_tactic.h feat(library/tactic): add generalize tactic, closes #34 2014-10-23 22:40:15 -07:00
goal.cpp refactor(library/tactic/inversion_tactic): add 'cases_on' step to inversion_tactic 2014-11-27 00:06:26 -08:00
goal.h refactor(library/tactic/inversion_tactic): add 'cases_on' step to inversion_tactic 2014-11-27 00:06:26 -08:00
init_module.cpp feat(library/tactic): add first step of 'inversion' tactic 2014-11-26 21:28:00 -08:00
init_module.h refactor(*): start move to explicit initialization/finalization, 2014-09-22 10:41:07 -07:00
intros_tactic.cpp refactor(library/tactic/intros_tactic): change approach for generating fresh names for nameless 'intros' 2014-11-26 21:27:09 -08:00
intros_tactic.h refactor(library/tactic/rename_tactic): use new 'tactic.expr' to implement 'intro/intros' tactic 2014-10-22 17:29:50 -07:00
inversion_tactic.cpp fix(library/tactic/inversion_tactic): bug in name generation 2014-11-28 14:51:12 -08:00
inversion_tactic.h feat(library/tactic): add first step of 'inversion' tactic 2014-11-26 21:28:00 -08:00
proof_state.cpp fix(library/tactic): pretty printer for proof states 2014-11-27 09:43:58 -08:00
proof_state.h fix(library/tactic): pretty printer for proof states 2014-11-27 09:43:58 -08:00
register_module.h refactor(library/tactic): simplify tactic framework, no more proof builders 2014-07-01 16:11:19 -07:00
rename_tactic.cpp refactor(frontends/lean): remove dead code 2014-10-22 17:39:06 -07:00
rename_tactic.h refactor(frontends/lean): remove dead code 2014-10-22 17:39:06 -07:00
revert_tactic.cpp refactor(library/tactic): cleanup 'revert' and 'clear' tactics 2014-11-26 17:08:14 -08:00
revert_tactic.h feat(library/tactic): add 'revert' tactic, closes #346 2014-11-26 14:23:42 -08:00
tactic.cpp feat(library/tactic): add rotate_left/rotate_right tactics, closes #278 2014-10-29 19:13:55 -07:00
tactic.h chore(library/tactic/tactic.h): cleanup 2014-11-27 09:15:49 -08:00
trace_tactic.cpp fix(library/tactic): pretty printer for proof states 2014-11-27 09:43:58 -08:00
trace_tactic.h refactor(library/tactic): move 'tracing' tactics to separate module 2014-10-22 14:12:45 -07:00
unfold_tactic.cpp refactor(library/tactic/unfold_tactic): use new 'tactic.expr' to implement 'unfold' tactic 2014-10-23 10:26:19 -07:00
unfold_tactic.h refactor(library/tactic): move 'unfold' tactic to separate module 2014-10-23 10:26:19 -07:00
util.cpp fix(library/tactic): add missing file 2014-10-23 14:04:12 -07:00
util.h fix(library/tactic): add missing file 2014-10-23 14:04:12 -07:00
whnf_tactic.cpp feat(library/tactic): add whnf tactic, closes #270 2014-10-28 23:18:49 -07:00
whnf_tactic.h feat(library/tactic): add whnf tactic, closes #270 2014-10-28 23:18:49 -07:00