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

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

Equations

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

def Lean.Meta.Split.simpMatch.pre (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

Equations

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

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

Equations

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

opaque Lean.Meta.Split.discrGenExId : Lean.InternalExceptionId

Internal exception for discriminant generalization failures due to type errors.

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

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

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