document @[match_pattern]

Author: Rob23oba

src/Lean/Meta/Match/MatchPatternAttr.lean

@@ -8,6 +8,25 @@ import Lean.Attributes
 
 namespace Lean
 
+/--
+Instructs the pattern matcher to unfold occurrences of this definition.
+
+By default, only constructors and literals can be used for pattern matching. Using
+`@[match_pattern]` allows using other definitions, as long as they eventually reduce to
+constructors.
+
+Example:
+```
+@[match_pattern]
+def yellowString : String := "yellow"
+
+def isYellow (color : String) : Bool :=
+  match color with
+  | yellowString => true
+  | _ => false
+```
+-/
+@[builtin_doc]
 builtin_initialize matchPatternAttr : TagAttribute ←
   registerTagAttribute `match_pattern "mark that a definition can be used in a pattern (remark: the dependent pattern matching compiler will unfold the definition)"