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.

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.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.