Helper functions for using the simplifier.

[TODO] Reunification of mkSimpContext' with core.

def Lean.Meta.Simp.mkEqSymm (e : Lean.Expr) (r : Lean.Meta.Simp.Result) : Lean.MetaM Lean.Meta.Simp.Result

Flip the proof in a Simp.Result.

Equations

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

def Lean.Meta.Simp.mkCast (r : Lean.Meta.Simp.Result) (e : Lean.Expr) : Lean.MetaM Lean.Expr

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]

abbrev Lean.Elab.Tactic.mkDischargeWrapper (optDischargeSyntax : Lean.Syntax) : Lean.Elab.Tactic.TacticM Lean.Elab.Tactic.Simp.DischargeWrapper

Construct a Simp.DischargeWrapper from the Syntax for a simp discharger.

Equations

• Lean.Elab.Tactic.mkDischargeWrapper = Lean.Elab.Tactic.mkDischargeWrapper✝

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) : Lean.Elab.Tactic.TacticM Lean.Elab.Tactic.MkSimpContextResult

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.