From e3e9220ab97f686cbe56b3b4d1db7f9e9b2e3f46 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 26 Jun 2015 18:41:08 -0700 Subject: [PATCH] fix(library/tactic/rewrite_tactic): fixes #708 --- src/library/tactic/rewrite_tactic.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index c72c9fbcb..60af7b540 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -1200,7 +1200,11 @@ class rewrite_fn { rule = mk_app(rule, meta); } rule_type = reduce_rule_type(rule_type); - lean_assert(is_eq(rule_type) || (is_standard(m_env) && is_iff(rule_type))); + if (!is_eq(rule_type) && !(is_standard(m_env) && is_iff(rule_type))) { + // Remark: this branch is reachable when the user provide explicit patterns. + throw_rewrite_exception("invalid rewrite tactic, given lemma is not an equality or iff"); + } + if (is_standard(m_env) && is_iff(rule_type)) { rule = apply_propext(rule, rule_type); rule_type = mk_eq(*m_relaxed_tc, app_arg(app_fn(rule_type)), app_arg(rule_type));