Helper functions around named patterns

def Lean.Meta.Match.mkNamedPattern (x h p : Expr) : MetaM Expr

Equations

• Lean.Meta.Match.mkNamedPattern x h p = Lean.Meta.mkAppM `namedPattern #[x, p, h]

def Lean.Meta.Match.isNamedPattern (e : Expr) : Bool

Equations

• Lean.Meta.Match.isNamedPattern e = (e.consumeMData.getAppNumArgs == 4 && e.consumeMData.getAppFn.consumeMData.isConstOf `namedPattern)

def Lean.Meta.Match.isNamedPattern? (e : Expr) : Option Expr

Equations

• Lean.Meta.Match.isNamedPattern? e = if (e.consumeMData.getAppNumArgs == 4 && e.consumeMData.getAppFn.consumeMData.isConstOf `namedPattern) = true then some e.consumeMData else none

def Lean.Meta.Match.unfoldNamedPattern (e : Expr) : MetaM Expr

Equations

• One or more equations did not get rendered due to their size.