inductive Lean.Meta.SplitKind : Type

• ite: Lean.Meta.SplitKind
• match: Lean.Meta.SplitKind
• both: Lean.Meta.SplitKind

def Lean.Meta.SplitKind.considerIte : Lean.Meta.SplitKind → Bool

def Lean.Meta.SplitKind.considerMatch : Lean.Meta.SplitKind → Bool

structure Lean.Meta.FindSplitImpl.Context : Type

• exceptionSet : Lean.ExprSet
• kind : Lean.Meta.SplitKind

@[reducible, inline]

unsafe abbrev Lean.Meta.FindSplitImpl.FindM (α : Type) : Type

@[inline]

unsafe def Lean.Meta.FindSplitImpl.checkVisited (e : Lean.Expr) : OptionT Lean.Meta.FindSplitImpl.FindM Unit

unsafe def Lean.Meta.FindSplitImpl.visit (e : Lean.Expr) : OptionT Lean.Meta.FindSplitImpl.FindM Lean.Expr

unsafe def Lean.Meta.FindSplitImpl.visit.visitApp? (e : Lean.Expr) : Lean.Meta.FindSplitImpl.FindM (Option Lean.Expr)

def Lean.Meta.findSplit? (e : Lean.Expr) (kind : Lean.Meta.SplitKind := Lean.Meta.SplitKind.both) (exceptionSet : Lean.ExprSet := ∅) : Lean.MetaM (Option Lean.Expr)

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

Equations

• Lean.Meta.findSplit? e kind exceptionSet = do let __do_lift ← Lean.instantiateMVars e Lean.Meta.findSplit?.go kind exceptionSet __do_lift

partial def Lean.Meta.findSplit?.go (kind : Lean.Meta.SplitKind := Lean.Meta.SplitKind.both) (exceptionSet : Lean.ExprSet := ∅) (e : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

def Lean.Meta.findSplit?.find? (kind : Lean.Meta.SplitKind := Lean.Meta.SplitKind.both) (exceptionSet : Lean.ExprSet := ∅) (e : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

def Lean.Meta.SplitIf.getSimpContext : Lean.MetaM Lean.Meta.Simp.Context

Default Simp.Context for simpIf methods. It contains all congruence theorems, but just the rewriting rules for reducing if expressions.

def Lean.Meta.SplitIf.mkDischarge? (useDecide : Bool := false) : Lean.MetaM Lean.Meta.Simp.Discharge

Equations

• Lean.Meta.SplitIf.mkDischarge? useDecide = do let __do_lift ← Lean.getLCtx pure (Lean.Meta.SplitIf.discharge?✝ __do_lift.numIndices useDecide)

def Lean.Meta.SplitIf.splitIfAt? (mvarId : Lean.MVarId) (e : Lean.Expr) (hName? : Option Lean.Name) : Lean.MetaM (Option (Lean.Meta.ByCasesSubgoal × Lean.Meta.ByCasesSubgoal))

Equations

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

def Lean.Meta.simpIfTarget (mvarId : Lean.MVarId) (useDecide : Bool := false) : Lean.MetaM Lean.MVarId

Equations

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

def Lean.Meta.simpIfLocalDecl (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) : Lean.MetaM Lean.MVarId

def Lean.Meta.splitIfTarget? (mvarId : Lean.MVarId) (hName? : Option Lean.Name := none) : Lean.MetaM (Option (Lean.Meta.ByCasesSubgoal × Lean.Meta.ByCasesSubgoal))

def Lean.Meta.splitIfLocalDecl? (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (hName? : Option Lean.Name := none) : Lean.MetaM (Option (Lean.MVarId × Lean.MVarId))

Equations

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