inductive Lean.Meta.SplitKind : Type

• ite : SplitKind
• match : SplitKind
• both : SplitKind

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

Equations

• Lean.Meta.SplitKind.ite.considerIte = true
• Lean.Meta.SplitKind.both.considerIte = true
• x✝.considerIte = false

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

Equations

• Lean.Meta.SplitKind.match.considerMatch = true
• Lean.Meta.SplitKind.both.considerMatch = true
• x✝.considerMatch = false

structure Lean.Meta.FindSplitImpl.Context : Type

• exceptionSet : ExprSet
• kind : SplitKind

@[reducible, inline]

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

Equations

• Lean.Meta.FindSplitImpl.FindM = ReaderT Lean.Meta.FindSplitImpl.Context (StateT (Lean.PtrSet Lean.Expr) Lean.MetaM)

@[inline]

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

Equations

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

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

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

Equations

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

def Lean.Meta.findSplit? (e : Expr) (kind : SplitKind := SplitKind.both) (exceptionSet : ExprSet := ∅) : MetaM (Option 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 : SplitKind := SplitKind.both) (exceptionSet : ExprSet := ∅) (e : Expr) : MetaM (Option Expr)

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

Equations

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

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

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

Equations

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

def Lean.Meta.SplitIf.mkDischarge? (useDecide : Bool := false) : MetaM 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 : MVarId) (e : Expr) (hName? : Option Name) : MetaM (Option (ByCasesSubgoal × ByCasesSubgoal))

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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