structure Lean.Meta.MatcherApp : Type

• matcherName : Name
• matcherLevels : Array Level
• uElimPos? : Option Nat
• discrInfos : Array Match.DiscrInfo
• params : Array Expr
• motive : Expr
• discrs : Array Expr
• altNumParams : Array Nat
• 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.toExpr (matcherApp : MatcherApp) : Expr

Equations

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