Documentation

Lean.Meta.Match.MatchPatternAttr

source
opaque Lean.matchPatternAttr:
Lean.TagAttribute
source
@[export lean_has_match_pattern_attribute]
def Lean.hasMatchPatternAttribute (env : Lean.Environment) (n : Lean.Name) :
Bool
Equations