structure Lean.Meta.MatcherApp extends Lean.Meta.MatcherInfo : Type

• numParams : Nat
• numDiscrs : Nat
• altInfos : Array AltParamInfo
• uElimPos? : Option Nat
• discrInfos : Array DiscrInfo
• overlaps : Overlaps
• matcherName : Name
• matcherLevels : Array Level
• params : Array Expr
• motive : Expr
• discrs : Array Expr
• alts : Array Expr
• remaining : Array Expr

def Lean.Meta.matchMatcherApp? {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m] (e : Expr) (alsoCasesOn : Bool := false) : m (Option MatcherApp)

Recognizes if e is a matcher application, and destructs it into the MatcherApp data structure.

This can optionally also treat casesOn recursor applications as a special case of matcher applications.

Equations

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

def Lean.Meta.MatcherApp.altNumParams (matcherApp : MatcherApp) : Array Nat

Equations

• matcherApp.altNumParams = matcherApp.altNumParams

def Lean.Meta.MatcherApp.toExpr (matcherApp : MatcherApp) : Expr

Equations

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