Documentation

Lean.Meta.Tactic.Split

Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
def Lean.Meta.Split.applyMatchSplitter (mvarId : Lean.MVarId) (matcherDeclName : Lean.Name) (us : ) (params : ) (discrs : ) :
Equations
• One or more equations did not get rendered due to their size.
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 : ) (exceptionSet : ) :

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

Equations
partial def Lean.Meta.Split.findSplit?.go (env : Lean.Environment) (splitIte : ) (exceptionSet : ) (e : Lean.Expr) :
def Lean.Meta.Split.findSplit?.isCandidate (env : Lean.Environment) (splitIte : ) (exceptionSet : ) (e : Lean.Expr) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.Meta.splitTarget? (mvarId : Lean.MVarId) (splitIte : ) :
Equations
• One or more equations did not get rendered due to their size.
partial def Lean.Meta.splitTarget?.go (mvarId : Lean.MVarId) (splitIte : ) (target : Lean.Expr) (badCases : Lean.ExprSet) :
Equations
• One or more equations did not get rendered due to their size.