opaque Lean.matchPatternAttr : TagAttribute

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 and literals.

Example:

@[match_pattern]
def yellowString : String := "yellow"

def isYellow (color : String) : Bool :=
  match color with
  | yellowString => true
  | _ => false

@[export lean_has_match_pattern_attribute]

def Lean.hasMatchPatternAttribute (env : Environment) (n : Name) : Bool

Equations

• Lean.hasMatchPatternAttribute env n = Lean.matchPatternAttr.hasTag env n