Documentation

Batteries.Lean.Meta.Simp

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.

Construct the Expr cast h e, from a Simp.Result with proof h.

Equations

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.