Default Simp.Context for simpIf methods. It contains all congruence theorems, but
just the rewriting rules for reducing if expressions.
Instances For
Default discharge? function for simpIf methods.
It only uses hypotheses from the local context. It is effective
after a case-split.
Instances For
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)
 :
Instances For
Instances For
Instances For
Instances For
def
Lean.Meta.splitIfLocalDecl?
(mvarId : Lean.MVarId)
(fvarId : Lean.FVarId)
(hName? : optParam (Option Lake.Name) none)
 :