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)
: