Documentation

Lean.Meta.Tactic.Split

source
def Lean.Meta.Split.getSimpMatchContext :
MetaM Simp.Context
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Split.simpMatch (e : Expr) :
MetaM Simp.Result
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Split.simpMatch.pre (e : Expr) :
SimpM Simp.Step
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Split.simpMatchTarget (mvarId : MVarId) :
MetaM MVarId
Equations
  • One or more equations did not get rendered due to their size.
source
opaque Lean.Meta.Split.discrGenExId :
InternalExceptionId

Internal exception for discriminant generalization failures due to type errors.

source
def Lean.Meta.Split.isDiscrGenException (ex : Exception) :
Bool
Equations
source
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.
source
def Lean.Meta.Split.mkDiscrGenErrorMsg (e : Expr) :
MessageData
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Split.throwDiscrGenError {α : Type} (e : Expr) :
MetaM α
Equations
source
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.
source
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.
source
partial def Lean.Meta.splitTarget?.go (mvarId : MVarId) (splitIte : Bool := true) (target : Expr) (badCases : ExprSet) :
MetaM (Option (List MVarId))
source
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.