opaque Lean.matchPatternAttr : Lean.TagAttribute

@[export lean_has_match_pattern_attribute]

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