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

feat(library/tactic/induction_tactic): new flavor of intron

Browse source
This commit is contained in:
Leonardo de Moura 2016-07-14 14:43:41 -04:00
parent 04fe48539f
commit d49ab7d220
2 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/tactic/intro_tactic.cpp
View file

@ -87,6 +87,12 @@ optional<expr> intron(environment const & env, options const & opts, metavar_con
return intron(env, opts, mctx, mvar, n, empty);
}
optional<expr> intron(environment const & env, options const & opts, metavar_context & mctx,
expr const & mvar, unsigned n, buffer<name> & new_Hns) {
list<name> empty;
return intron(env, opts, mctx, mvar, n, empty, new_Hns);
}
optional<tactic_state> intron(unsigned n, tactic_state const & s, buffer<name> & new_Hns) {
if (n == 0) return some_tactic_state(s);
optional<expr> mvar = s.get_main_goal();

2
src/library/tactic/intro_tactic.h
View file

@ -18,6 +18,8 @@ optional<expr> intron(environment const & env, options const & opts, metavar_con
expr const & mvar, unsigned n, list<name> & new_hs_names, buffer<name> & new_Hns);
optional<expr> intron(environment const & env, options const & opts, metavar_context & mctx,
expr const & mvar, unsigned n, list<name> & new_hs_names);
optional<expr> intron(environment const & env, options const & opts, metavar_context & mctx,
expr const & mvar, unsigned n, buffer<name> & new_Hns);
optional<expr> intron(environment const & env, options const & opts, metavar_context & mctx,
expr const & mvar, unsigned n);