From efcebc60f787b68f4e882b440f761550cb42e057 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 16 Feb 2017 21:43:34 -0800 Subject: [PATCH] feat(library/init/meta/contradiction_tactic): make it more robust --- library/init/meta/contradiction_tactic.lean | 2 +- tests/lean/run/contradiction_issue.lean | 5 +++++ 2 files changed, 6 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/contradiction_issue.lean diff --git a/library/init/meta/contradiction_tactic.lean b/library/init/meta/contradiction_tactic.lean index 33cdfcd074..7af421523e 100644 --- a/library/init/meta/contradiction_tactic.lean +++ b/library/init/meta/contradiction_tactic.lean @@ -34,7 +34,7 @@ private meta def contra_false : list expr → tactic unit private meta def contra_not_a_refl_rel_a : list expr → tactic unit | [] := failed | (H :: Hs) := - do t ← infer_type H, + do t ← infer_type H >>= beta, (do (lhs, rhs) ← match_ne t, unify lhs rhs, tgt ← target, diff --git a/tests/lean/run/contradiction_issue.lean b/tests/lean/run/contradiction_issue.lean new file mode 100644 index 0000000000..2fdb1bd81b --- /dev/null +++ b/tests/lean/run/contradiction_issue.lean @@ -0,0 +1,5 @@ +open tactic + +def hd {α} : {l : list α // l ≠ []} → α +| ⟨[], h⟩ := by contradiction +| ⟨a::l, h⟩ := a