Helper functions for using the simplifier. #
[TODO] Reunification of mkSimpContext'
with core.
Flip the proof in a Simp.Result
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Construct the Expr
cast h e
, from a Simp.Result
with proof h
.
Equations
- Lean.Meta.Simp.mkCast r e = do let __do_lift ← r.getProof Lean.Meta.mkAppM `cast #[__do_lift, e]
Instances For
Construct a Simp.DischargeWrapper
from the Syntax
for a simp
discharger.
Instances For
def
Lean.Meta.Simp.mkSimpContext'
(simpTheorems : Lean.Meta.SimpTheorems)
(stx : Lean.Syntax)
(eraseLocal : Bool)
(kind : Lean.Elab.Tactic.SimpKind := Lean.Elab.Tactic.SimpKind.simp)
(ctx ignoreStarArg : Bool := false)
:
If ctx == false
, the config argument is assumed to have type Meta.Simp.Config
,
and Meta.Simp.ConfigCtx
otherwise.
If ctx == false
, the discharge
option must be none
Equations
- One or more equations did not get rendered due to their size.