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.
Instances For

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

    Equations
    Instances For

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

      Equations
      Instances For

        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.
        Instances For