Test case for tests/lean/run/issue11449.lean

Author: nomeata

tests/lean/run/issue11449.lean

@@ -0,0 +1,29 @@
+opaque double : Nat → Nat
+
+inductive Parity : Nat -> Type
+| even (n) : Parity (double n)
+| odd  (n) : Parity (Nat.succ (double n))
+
+example
+  (motive : (x : Nat) → Parity x → Sort u_1)
+  (h_2 : (j : Nat) → motive (double j) (Parity.even j))
+  (j n : Nat)
+  (heq_1 : double n = double j)
+  (heq_2 : Parity.even n ≍ Parity.even j):
+  h_2 n ≍ h_2 j := by
+  fail_if_success grind -- does not work yet
+  sorry
+
+-- manual proof using heterogenenous noConfusion
+
+example
+  (motive : (x : Nat) → Parity x → Sort u_1)
+  (h_2 : (j : Nat) → motive (double j) (Parity.even j))
+  (j n : Nat)
+  (heq_1 : double n = double j)
+  (heq_2 : Parity.even n ≍ Parity.even j):
+  h_2 n ≍ h_2 j := by
+  apply Parity.noConfusion heq_1 heq_2
+  intro hnj
+  subst hnj
+  rfl

tests/lean/run/structuralMutual.lean

@@ -512,13 +512,13 @@ Too many possible combinations of parameters of type Nattish (or please indicate
 Could not find a decreasing measure.
 The basic measures relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
-Call from ManyCombinations.f to ManyCombinations.g at 543:15-29:
+Call from ManyCombinations.f to ManyCombinations.g at 544:15-29:
    #1 #2 #3 #4
 #5  ?  ?  ?  ?
 #6  ?  ?  =  ?
 #7  ?  ?  ?  =
 #8  ?  =  ?  ?
-Call from ManyCombinations.g to ManyCombinations.f at 546:15-29:
+Call from ManyCombinations.g to ManyCombinations.f at 547:15-29:
    #5 #6 #7 #8
 #1  _  _  _  _
 #2  _  _  _  ?