diff --git a/src/Init/Grind/Norm.lean b/src/Init/Grind/Norm.lean index 8a35d84467..78a25ff386 100644 --- a/src/Init/Grind/Norm.lean +++ b/src/Init/Grind/Norm.lean @@ -106,6 +106,7 @@ init_grind_norm or_true true_or or_false false_or or_assoc -- ite ite_true ite_false ite_true_false ite_false_true + dite_eq_ite -- Forall forall_and -- Exists diff --git a/tests/lean/run/grind_t1.lean b/tests/lean/run/grind_t1.lean index 848f6fff2c..6a4691b9e3 100644 --- a/tests/lean/run/grind_t1.lean +++ b/tests/lean/run/grind_t1.lean @@ -393,3 +393,6 @@ example [Decidable p] : a = true → p → decide p = a := by example [Decidable p] : false = a → ¬p → decide p = a := by grind + +example (a : Nat) (p q r : Prop) (h₁ : if _ : a < 1 then p else q) (h₂ : r) : (if a < 1 then p else q) ↔ r := by + grind (splits := 0)