Documentation

LeanCert.Tactic.IntervalAuto.Extract

Rational Extraction Utilities #

Utilities for extracting rational numbers from Lean expressions representing real number literals or coercions.

source
def LeanCert.Tactic.Auto.extractRatFromReal (e : Lean.Expr) :
Lean.MetaM (Option ℚ)

Try to extract a rational value from a normalized real-number expression.

Equations
Instances For
    source
    def LeanCert.Tactic.Auto.mkIntervalRat (loExpr hiExpr : Lean.Expr) (lo hi : ℚ) :
    Lean.MetaM Lean.Expr

    Build an IntervalRat expression from two rational expressions and their Lean representations

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def LeanCert.Tactic.Auto.toRat? (e : Lean.Expr) :
      Lean.MetaM (Option ℚ)

      Try to convert an expression directly to a rational (if it IS a rational constant)

      Equations
      Instances For