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.simpMatch.pre (e : Expr) : SimpM Simp.Step

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 { entries := [] }) = (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) : MetaM (Option (List MVarId))

Equations

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

partial def Lean.Meta.splitTarget?.go (mvarId : MVarId) (splitIte : Bool := true) (target : Expr) (badCases : ExprSet) : MetaM (Option (List MVarId))

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.