Documentation

LeanCert.Tactic.IntervalAuto.Extract

Rational Extraction Utilities #

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

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

Try to extract a rational value from a Lean expression that represents a real number. Handles: Rat.cast, OfNat.ofNat, Nat.cast, Int.cast, negations, and divisions. Also handles direct ℚ expressions as a fallback.

source
partial def LeanCert.Tactic.Auto.extractRatFromReal.tryExtract (e : Lean.Expr) :
Lean.MetaM (Option ℚ)
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