From 7eed45dd45e5f73eb3aaa618cf86a5041949e24b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 15 Aug 2020 07:59:31 -0700
Subject: [PATCH] fix: generalize `isNatValueTransition`

---
 src/Lean/Meta/EqnCompiler/DepElim.lean | 10 +++++++---
 tests/lean/match2.lean                 |  4 ++--
 2 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Meta/EqnCompiler/DepElim.lean b/src/Lean/Meta/EqnCompiler/DepElim.lean
index 11cf52fa60..4ac0efb133 100644
--- a/src/Lean/Meta/EqnCompiler/DepElim.lean
+++ b/src/Lean/Meta/EqnCompiler/DepElim.lean
@@ -293,8 +293,12 @@ hasArrayLitPattern p && hasVarPattern p
    | Pattern.var _ :: _        => true
    | _                         => false
 
-private def isNatValueCtorTransition (p : Problem) : Bool :=
-hasCtorPattern p && hasNatValPattern p
+private def isNatValueTransition (p : Problem) : Bool :=
+hasNatValPattern p
+&& p.alts.any fun alt => match alt.patterns with
+   | Pattern.ctor _ _ _ _ :: _   => true
+   | Pattern.inaccessible _ :: _ => true
+   | _                           => false
 
 private def processNonVariable (p : Problem) : Problem :=
 match p.vars with
@@ -618,7 +622,7 @@ private partial def process : Problem → StateT State MetaM Unit
   else if isArrayLitTransition p then do
     ps ← liftM $ processArrayLit p;
     ps.forM process
-  else if isNatValueCtorTransition p then do
+  else if isNatValueTransition p then do
     traceStep ("nat value to constructor");
     process (expandNatValuePattern p)
   else
diff --git a/tests/lean/match2.lean b/tests/lean/match2.lean
index 09ce13b3dc..a2cbb8a0fc 100644
--- a/tests/lean/match2.lean
+++ b/tests/lean/match2.lean
@@ -11,8 +11,8 @@ structure Node : Type :=
 
 def h1 (x : List Node) : Bool :=
 match x with
-| _ :: Node.mk _ _ (Op.mk Nat.zero) :: _  => true
-| _                                       => false
+| _ :: Node.mk _ _ (Op.mk 0) :: _  => true
+| _                                => false
 
 def mkNode (n : Nat) : Node := { id₁ := n, id₂ := n, o := Op.mk n }