max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/tactic/tactic_state): add helper mk procedure

Browse source
This commit is contained in:
Leonardo de Moura 2016-07-27 13:42:32 -07:00
parent 9477b91978
commit 1b75a98ea4
2 changed files with 11 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/library/tactic/tactic_state.cpp
View file

@ -44,12 +44,17 @@ optional<metavar_decl> tactic_state::get_main_goal_decl() const {
return mctx().get_metavar_decl(head(goals()));
}
tactic_state mk_tactic_state_for(environment const & env, options const & o, local_context const & lctx, expr const & type) {
metavar_context mctx;
tactic_state mk_tactic_state_for(environment const & env, options const & o, metavar_context mctx,
local_context const & lctx, expr const & type) {
expr main = mctx.mk_metavar_decl(lctx, type);
return tactic_state(env, o, mctx, list<expr>(main), main);
}
tactic_state mk_tactic_state_for(environment const & env, options const & o, local_context const & lctx, expr const & type) {
metavar_context mctx;
return mk_tactic_state_for(env, o, mctx, lctx, type);
}
tactic_state set_options(tactic_state const & s, options const & o) {
return tactic_state(s.env(), o, s.mctx(), s.goals(), s.main());
}

5
src/library/tactic/tactic_state.h
View file

@ -73,7 +73,10 @@ inline optional<tactic_state> none_tactic_state() { return optional<tactic_state
inline optional<tactic_state> some_tactic_state(tactic_state const & e) { return optional<tactic_state>(e); }
inline optional<tactic_state> some_tactic_state(tactic_state && e) { return optional<tactic_state>(std::forward<tactic_state>(e)); }
tactic_state mk_tactic_state_for(environment const & env, options const & opts, local_context const & lctx, expr const & type);
tactic_state mk_tactic_state_for(environment const & env, options const & opts, metavar_context mctx,
local_context const & lctx, expr const & type);
tactic_state mk_tactic_state_for(environment const & env, options const & opts,
local_context const & lctx, expr const & type);
tactic_state set_options(tactic_state const & s, options const & o);
tactic_state set_env(tactic_state const & s, environment const & env);