Rational Extraction Utilities

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

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.

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

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.

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

• LeanCert.Tactic.Auto.toRat? e = do let __do_lift ← LeanCert.Meta.toRat? e match __do_lift with | some q => pure (some q) | none => LeanCert.Tactic.Auto.extractRatFromReal e