feat: attribute [grind cases eager] PProd MProd

2026-03-17 18:34:06 +00:00 · 2025-07-01 13:49:34 +10:00
1 changed files with 1 additions and 1 deletions
--- a/src/Init/Grind/Cases.lean
+++ b/src/Init/Grind/Cases.lean
@@ -11,5 +11,5 @@ public import Init.Grind.Tactics

 public section

-attribute [grind cases eager] And Prod False Empty True PUnit Exists Subtype
+attribute [grind cases eager] And False Empty True PUnit Exists Subtype Prod PProd MProd
 attribute [grind cases] Or