bug(ext): failure on ext lemmas with no hypotheses (leanprover-commun…

…ity#269)
spl · Aug 22, 2018 · 58cfe9f · 58cfe9f
1 parent d18a3a8
commit 58cfe9f
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 1 deletion.
diff --git a/tactic/basic.lean b/tactic/basic.lean
@@ -299,7 +299,7 @@ do h' ← assert h p,
    return (h', gs)
 
 meta def try_intros : list name → tactic (list name)
-| [] := intros $> []
+| [] := try intros $> []
 | (x::xs) := (intro x >> try_intros xs) <|> pure (x :: xs)
 
 meta def ext1 (xs : list name) : tactic (list name) :=

diff --git a/tests/tactics.lean b/tests/tactics.lean
@@ -339,6 +339,16 @@ end rcases
 
 section ext
 
+@[extensionality] lemma unit.ext (x y : unit) : x = y :=
+begin
+  cases x, cases y, refl
+end
+
+example : subsingleton unit :=
+begin
+  split, intros, ext
+end
+
 example (x y : ℕ) : true :=
 begin
   have : x = y,