michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean): add unfold tactic command

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-29 12:05:45 -07:00
parent 937d7b2813
commit 2510d5722a
2 changed files with 15 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/frontends/lean/builtin_tactic_cmds.cpp
View file

@ -17,6 +17,14 @@ tactic parse_id_tactic(parser &) { return id_tactic(); }
tactic parse_now_tactic(parser &) { return now_tactic(); }
tactic parse_show_tactic(parser &) { return trace_state_tactic(); }
tactic parse_assumption_tactic(parser &) { return assumption_tactic(); }
tactic parse_unfold_tactic(parser & p) {
auto pos = p.pos();
expr id = p.parse_expr();
if (!is_constant(id))
throw parser_error("invalid 'unfold' tactic, constant expected", pos);
return unfold_tactic(const_name(id));
}
tactic parse_echo_tactic(parser & p) {
if (!p.curr_is_string())
throw parser_error("invalid 'echo' tactic, string expected", p.pos());
@ -60,6 +68,7 @@ tactic_cmd_table get_builtin_tactic_cmds() {
add_tactic(t, tactic_cmd_info("show", "show goals tactic", parse_show_tactic));
add_tactic(t, tactic_cmd_info("now", "succeeds only if all goals have been solved", parse_now_tactic));
add_tactic(t, tactic_cmd_info("echo", "trace tactic: display message", parse_echo_tactic));
add_tactic(t, tactic_cmd_info("unfold", "unfold definition", parse_unfold_tactic));
add_tactic(t, tactic_cmd_info("id", "do nothing tactic", parse_id_tactic));
add_tactic(t, tactic_cmd_info("assumption", "solve goal if there is an assumption that is identical to the conclusion",
parse_assumption_tactic));

6
tests/lean/run/tactic4.lean Normal file
View file

@ -0,0 +1,6 @@
import logic
definition id {A : Type} (a : A) := a
theorem tst {A B : Bool} (H1 : A) (H2 : B) : id A
:= by [unfold id, show, exact]