From 33cb9382aaf581a9b8a6d9bec886707a32b813ba Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 29 Jun 2014 19:41:54 -0700 Subject: [PATCH] feat(frontends/lean): add beta-reduction tactic command Signed-off-by: Leonardo de Moura --- src/frontends/lean/builtin_tactic_cmds.cpp | 2 ++ tests/lean/run/tactic9.lean | 4 ++++ 2 files changed, 6 insertions(+) create mode 100644 tests/lean/run/tactic9.lean diff --git a/src/frontends/lean/builtin_tactic_cmds.cpp b/src/frontends/lean/builtin_tactic_cmds.cpp index 95b29e95c..330c08c2d 100644 --- a/src/frontends/lean/builtin_tactic_cmds.cpp +++ b/src/frontends/lean/builtin_tactic_cmds.cpp @@ -12,6 +12,7 @@ static name g_bang("!"); tactic parse_fail_tactic(parser &, pos_info const &) { return fail_tactic(); } tactic parse_id_tactic(parser &, pos_info const &) { return id_tactic(); } tactic parse_now_tactic(parser &, pos_info const &) { return now_tactic(); } +tactic parse_beta_tactic(parser &, pos_info const &) { return beta_tactic(); } tactic parse_print_tactic(parser & p, pos_info const & pos) { return trace_state_tactic(p.get_stream_name(), pos); } @@ -54,6 +55,7 @@ tactic_cmd_table get_builtin_tactic_cmds() { 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("repeat", "repeat tactic", parse_repeat_tactic)); + add_tactic(t, tactic_cmd_info("beta", "beta-reduction tactic", parse_beta_tactic)); add_tactic(t, tactic_cmd_info("apply", "apply tactic", parse_apply_tactic)); add_tactic(t, tactic_cmd_info("!", "repeat tactic", parse_repeat_tactic)); add_tactic(t, tactic_cmd_info("id", "do nothing tactic", parse_id_tactic)); diff --git a/tests/lean/run/tactic9.lean b/tests/lean/run/tactic9.lean new file mode 100644 index 000000000..c217dcbc7 --- /dev/null +++ b/tests/lean/run/tactic9.lean @@ -0,0 +1,4 @@ +import logic + +theorem tst {A B : Bool} (H1 : A) (H2 : B) : ((fun x : Bool, x) A) ∧ B ∧ A +:= by (apply and_intro, beta, exact, apply and_intro, !exact)