diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index ae66706282..fa323a1bc8 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -35,9 +35,7 @@ definition eassumption : tactic := builtin definition state : tactic := builtin definition fail : tactic := builtin definition id : tactic := builtin -definition beta : tactic := builtin definition info : tactic := builtin -definition whnf : tactic := builtin definition contradiction : tactic := builtin definition exfalso : tactic := builtin definition congruence : tactic := builtin diff --git a/library/init/tactic.lean b/library/init/tactic.lean index 83047789ea..3e0df32247 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -35,9 +35,7 @@ definition eassumption : tactic := builtin definition state : tactic := builtin definition fail : tactic := builtin definition id : tactic := builtin -definition beta : tactic := builtin definition info : tactic := builtin -definition whnf : tactic := builtin definition contradiction : tactic := builtin definition exfalso : tactic := builtin definition congruence : tactic := builtin diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 0724ebf868..dc721c83fd 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -1,7 +1,7 @@ add_library(tactic OBJECT goal.cpp proof_state.cpp tactic.cpp elaborate.cpp apply_tactic.cpp intros_tactic.cpp rename_tactic.cpp trace_tactic.cpp exact_tactic.cpp generalize_tactic.cpp inversion_tactic.cpp -whnf_tactic.cpp revert_tactic.cpp assert_tactic.cpp clear_tactic.cpp +revert_tactic.cpp assert_tactic.cpp clear_tactic.cpp expr_to_tactic.cpp location.cpp rewrite_tactic.cpp util.cpp init_module.cpp change_tactic.cpp check_expr_tactic.cpp note_tactic.cpp contradiction_tactic.cpp exfalso_tactic.cpp constructor_tactic.cpp diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index c1c8b6b7a3..84b086c665 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -393,8 +393,6 @@ void initialize_expr_to_tactic() { []() { return now_tactic(); }); register_simple_tac(get_tactic_fail_name(), []() { return fail_tactic(); }); - register_simple_tac(get_tactic_beta_name(), - []() { return beta_tactic(); }); register_bin_tac(get_tactic_and_then_name(), [](tactic const & t1, tactic const & t2) { return then(t1, t2); }); register_bin_tac(get_tactic_par_name(), diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index 759c1b3835..d7002c8d7b 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -13,7 +13,6 @@ Author: Leonardo de Moura #include "library/tactic/trace_tactic.h" #include "library/tactic/exact_tactic.h" #include "library/tactic/generalize_tactic.h" -#include "library/tactic/whnf_tactic.h" #include "library/tactic/clear_tactic.h" #include "library/tactic/revert_tactic.h" #include "library/tactic/inversion_tactic.h" @@ -45,7 +44,6 @@ void initialize_tactic_module() { initialize_trace_tactic(); initialize_exact_tactic(); initialize_generalize_tactic(); - initialize_whnf_tactic(); initialize_clear_tactic(); initialize_revert_tactic(); initialize_inversion_tactic(); @@ -88,7 +86,6 @@ void finalize_tactic_module() { finalize_inversion_tactic(); finalize_revert_tactic(); finalize_clear_tactic(); - finalize_whnf_tactic(); finalize_generalize_tactic(); finalize_exact_tactic(); finalize_trace_tactic(); diff --git a/src/library/tactic/whnf_tactic.cpp b/src/library/tactic/whnf_tactic.cpp deleted file mode 100644 index 23a140b00d..0000000000 --- a/src/library/tactic/whnf_tactic.cpp +++ /dev/null @@ -1,43 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "library/constants.h" -#include "library/reducible.h" -#include "library/tactic/expr_to_tactic.h" -#include "library/tactic/elaborate.h" -#include "library/tactic/whnf_tactic.h" - -namespace lean { -tactic whnf_tactic() { - return tactic01([=](environment const & env, io_state const & ios, proof_state const & ps) { - goals const & gs = ps.get_goals(); - if (empty(gs)) - return none_proof_state(); - auto tc = mk_type_checker(env); - goal g = head(gs); - goals tail_gs = tail(gs); - expr type = g.get_type(); - auto t_cs = tc->whnf(type); - goals new_gs(goal(g.get_meta(), t_cs.first), tail_gs); - proof_state new_ps(ps, new_gs); - if (solve_constraints(env, ios, new_ps, t_cs.second)) { - return some_proof_state(new_ps); - } else { - return none_proof_state(); - } - }); -} - -void initialize_whnf_tactic() { - register_tac(get_tactic_whnf_name(), - [](old_type_checker &, elaborate_fn const &, expr const &, pos_info_provider const *) { - return whnf_tactic(); - }); -} - -void finalize_whnf_tactic() { -} -} diff --git a/src/library/tactic/whnf_tactic.h b/src/library/tactic/whnf_tactic.h deleted file mode 100644 index 0ad5c0e6ab..0000000000 --- a/src/library/tactic/whnf_tactic.h +++ /dev/null @@ -1,14 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "library/tactic/tactic.h" - -namespace lean { -tactic whnf_tactic(); -void initialize_whnf_tactic(); -void finalize_whnf_tactic(); -} diff --git a/tests/lean/whnf_tac.lean b/tests/lean/whnf_tac.lean deleted file mode 100644 index e099311e8a..0000000000 --- a/tests/lean/whnf_tac.lean +++ /dev/null @@ -1,11 +0,0 @@ -import logic - --- definition id {A : Type} (a : A) := a - -theorem tst (a : Prop) : a → id a := -begin - intro Ha, - whnf, - state, - apply Ha -end diff --git a/tests/lean/whnf_tac.lean.expected.out b/tests/lean/whnf_tac.lean.expected.out deleted file mode 100644 index 6344990479..0000000000 --- a/tests/lean/whnf_tac.lean.expected.out +++ /dev/null @@ -1,4 +0,0 @@ -whnf_tac.lean:9:2: proof state -a : Prop, -Ha : a -⊢ a