opaque Lean.Meta.SplitIf.ext : Lean.LazyInitExtension Lean.MetaM Lean.Meta.Simp.Context

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.

Equations

• Lean.Meta.SplitIf.getSimpContext = Lean.LazyInitExtension.get Lean.Meta.SplitIf.ext

def Lean.Meta.SplitIf.mkDischarge? (useDecide : optParam 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? (Lean.LocalContext.numIndices __do_lift) useDecide)

partial def Lean.Meta.SplitIf.findIfToSplit? (e : Lean.Expr) : Option Lean.Expr

Return the condition of an if expression to case split.

def Lean.Meta.SplitIf.splitIfAt? (mvarId : Lean.MVarId) (e : Lean.Expr) (hName? : Option Lake.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 : optParam 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

Equations

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

def Lean.Meta.splitIfTarget? (mvarId : Lean.MVarId) (hName? : optParam (Option Lake.Name) none) : 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.splitIfLocalDecl? (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (hName? : optParam (Option Lake.Name) none) : Lean.MetaM (Option (Lean.MVarId × Lean.MVarId))

Equations

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