structure Lean.Meta.MatcherApp : Type

• matcherName : Lean.Name
• matcherLevels : Array Lean.Level
• uElimPos? : Option Nat
• discrInfos : Array Lean.Meta.Match.DiscrInfo
• params : Array Lean.Expr
• motive : Lean.Expr
• discrs : Array Lean.Expr
• altNumParams : Array Nat
• alts : Array Lean.Expr
• remaining : Array Lean.Expr

def Lean.Meta.matchMatcherApp? {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] (e : Lean.Expr) (alsoCasesOn : Bool := false) : m (Option Lean.Meta.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 : Lean.Meta.MatcherApp) : Lean.Expr