michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/tactic/inversion_tactic): improve error message for unknown hypothesis

Browse source
This commit is contained in:
Leonardo de Moura 2015-03-13 15:19:19 -07:00
parent b88b98ac22
commit aba158dbd4
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/tactic/inversion_tactic.cpp
View file

@ -1037,8 +1037,11 @@ public:
optional<result> execute(goal const & g, name const & n, implementation_list const & imps) { optional<result> execute(goal const & g, name const & n, implementation_list const & imps) {
auto p = g.find_hyp(n); auto p = g.find_hyp(n);
if (!p) if (!p) {
if (m_throw_tactic_exception)
throw tactic_exception(sstream() << "invalid 'cases' tactic, unknown hypothesis '" << n << "'");
return optional<result>(); return optional<result>();
}
expr const & h = p->first; expr const & h = p->first;
return execute(g, h, imps); return execute(g, h, imps);
} }