feat: grind_pattern for Subtype.property

2026-03-17 18:34:06 +00:00 · 2025-11-22 11:19:07 +11:00
1 changed files with 2 additions and 0 deletions
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -631,6 +631,8 @@ structure Subtype {α : Sort u} (p : α → Prop) where
  -/
  property : p val

+grind_pattern Subtype.property => self.val
+
 set_option linter.unusedVariables.funArgs false in
 /--
 Gadget for optional parameter support.