refactor(library/tactic): rename boolean.* to boolean_tactics.*
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
fa98c1358f
commit
43ef8b9a4b
5 changed files with 6 additions and 6 deletions
|
@ -1,4 +1,4 @@
|
||||||
add_library(tactic goal.cpp proof_builder.cpp cex_builder.cpp
|
add_library(tactic goal.cpp proof_builder.cpp cex_builder.cpp
|
||||||
proof_state.cpp tactic.cpp boolean.cpp apply_tactic.cpp)
|
proof_state.cpp tactic.cpp boolean_tactics.cpp apply_tactic.cpp)
|
||||||
|
|
||||||
target_link_libraries(tactic ${LEAN_LIBS})
|
target_link_libraries(tactic ${LEAN_LIBS})
|
||||||
|
|
|
@ -386,7 +386,7 @@ static int mk_absurd_tactic(lua_State * L) {
|
||||||
return push_tactic(L, absurd_tactic());
|
return push_tactic(L, absurd_tactic());
|
||||||
}
|
}
|
||||||
|
|
||||||
void open_boolean(lua_State * L) {
|
void open_boolean_tactics(lua_State * L) {
|
||||||
SET_GLOBAL_FUN(mk_conj_tactic, "conj_tactic");
|
SET_GLOBAL_FUN(mk_conj_tactic, "conj_tactic");
|
||||||
SET_GLOBAL_FUN(mk_imp_tactic, "imp_tactic");
|
SET_GLOBAL_FUN(mk_imp_tactic, "imp_tactic");
|
||||||
SET_GLOBAL_FUN(mk_conj_hyp_tactic, "conj_hyp_tactic");
|
SET_GLOBAL_FUN(mk_conj_hyp_tactic, "conj_hyp_tactic");
|
|
@ -17,5 +17,5 @@ tactic disj_tactic();
|
||||||
tactic disj_tactic(unsigned i);
|
tactic disj_tactic(unsigned i);
|
||||||
tactic disj_tactic(name const & gname);
|
tactic disj_tactic(name const & gname);
|
||||||
tactic absurd_tactic();
|
tactic absurd_tactic();
|
||||||
void open_boolean(lua_State * L);
|
void open_boolean_tactics(lua_State * L);
|
||||||
}
|
}
|
|
@ -11,7 +11,7 @@ Author: Leonardo de Moura
|
||||||
#include "library/tactic/cex_builder.h"
|
#include "library/tactic/cex_builder.h"
|
||||||
#include "library/tactic/proof_state.h"
|
#include "library/tactic/proof_state.h"
|
||||||
#include "library/tactic/tactic.h"
|
#include "library/tactic/tactic.h"
|
||||||
#include "library/tactic/boolean.h"
|
#include "library/tactic/boolean_tactics.h"
|
||||||
#include "library/tactic/apply_tactic.h"
|
#include "library/tactic/apply_tactic.h"
|
||||||
|
|
||||||
namespace lean {
|
namespace lean {
|
||||||
|
@ -21,7 +21,7 @@ inline void open_tactic_module(lua_State * L) {
|
||||||
open_cex_builder(L);
|
open_cex_builder(L);
|
||||||
open_proof_state(L);
|
open_proof_state(L);
|
||||||
open_tactic(L);
|
open_tactic(L);
|
||||||
open_boolean(L);
|
open_boolean_tactics(L);
|
||||||
open_apply_tactic(L);
|
open_apply_tactic(L);
|
||||||
}
|
}
|
||||||
inline void register_tactic_module() {
|
inline void register_tactic_module() {
|
||||||
|
|
|
@ -14,7 +14,7 @@ Author: Leonardo de Moura
|
||||||
#include "library/tactic/proof_builder.h"
|
#include "library/tactic/proof_builder.h"
|
||||||
#include "library/tactic/proof_state.h"
|
#include "library/tactic/proof_state.h"
|
||||||
#include "library/tactic/tactic.h"
|
#include "library/tactic/tactic.h"
|
||||||
#include "library/tactic/boolean.h"
|
#include "library/tactic/boolean_tactics.h"
|
||||||
using namespace lean;
|
using namespace lean;
|
||||||
|
|
||||||
tactic loop_tactic() {
|
tactic loop_tactic() {
|
||||||
|
|
Loading…
Reference in a new issue