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

Equations

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

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

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 : Lean.MVarId) (matcherDeclName : Lake.Name) (us : Array Lean.Level) (params : Array Lean.Expr) (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

Equations

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

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.Split.findSplit? (env : Lean.Environment) (e : Lean.Expr) (splitIte : optParam Bool true) (exceptionSet : optParam Lean.ExprSet ∅) : Option Lean.Expr

Return an if-then-else or match-expr to split.

Equations

• Lean.Meta.Split.findSplit? env e splitIte exceptionSet = Lean.Meta.Split.findSplit?.go env splitIte exceptionSet e

partial def Lean.Meta.Split.findSplit?.go (env : Lean.Environment) (splitIte : optParam Bool true) (exceptionSet : optParam Lean.ExprSet ∅) (e : Lean.Expr) : Option Lean.Expr

def Lean.Meta.Split.findSplit?.isCandidate (env : Lean.Environment) (splitIte : optParam Bool true) (exceptionSet : optParam Lean.ExprSet ∅) (e : Lean.Expr) : Bool

Equations

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

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

Equations

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

partial def Lean.Meta.splitTarget?.go (mvarId : Lean.MVarId) (splitIte : optParam 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))

Equations

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