opaque Lean.matchPatternAttr : Lean.TagAttribute

@[export lean_has_match_pattern_attribute]

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

Equations

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