def Lean.Meta.Split.getSimpMatchContext : MetaM Simp.Context

Equations

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

def Lean.Meta.Split.simpMatch (e : Expr) : MetaM Simp.Result

Equations

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

def Lean.Meta.Split.simpMatchTarget (mvarId : MVarId) : MetaM MVarId

Equations

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

opaque Lean.Meta.Split.discrGenExId : InternalExceptionId

Internal exception for discriminant generalization failures due to type errors.

def Lean.Meta.Split.isDiscrGenException (ex : Exception) : Bool

Equations

• Lean.Meta.Split.isDiscrGenException (Lean.Exception.internal id) = (id == Lean.Meta.Split.discrGenExId)
• Lean.Meta.Split.isDiscrGenException ex = false

def Lean.Meta.Split.applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Level) (params discrs : Array Expr) : MetaM (List MVarId)

Equations

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

def Lean.Meta.Split.mkDiscrGenErrorMsg (e : Expr) : MessageData

Equations

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

def Lean.Meta.Split.throwDiscrGenError {α : Type} (e : Expr) : MetaM α

Equations

• Lean.Meta.Split.throwDiscrGenError e = Lean.throwError (Lean.Meta.Split.mkDiscrGenErrorMsg e)

def Lean.Meta.Split.splitMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId)

Equations

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

def Lean.Meta.splitTarget? (mvarId : MVarId) (splitIte : Bool := true) (useNewSemantics : Bool := false) : MetaM (Option (List MVarId))

Splits an if-then-else of match-expression in the goal target. If useNewSemantics is true, the flag backward.split is ignored. Recall this flag only affects the split of if-then-else expressions.

Equations

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

def Lean.Meta.splitLocalDecl? (mvarId : MVarId) (fvarId : FVarId) : MetaM (Option (List MVarId))

Equations

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