Skip to content

Commit 26b435f

Browse files
authored
feat: grind_pattern for Subtype.property (#11317)
This PR adds `grind_pattern Subtype.property => self.val`.
1 parent fd4ff1f commit 26b435f

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

src/Init/Prelude.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -631,6 +631,8 @@ structure Subtype {α : Sort u} (p : α → Prop) where
631631
-/
632632
property : p val
633633

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

0 commit comments

Comments
 (0)