Meta-level Numeral Extraction

Utilities for extracting rational constants from elaborated Lean expressions. The goal is to support multiple equivalent syntactic encodings (literals, casts, scientific notation, arithmetic on constants) in one place.

def LeanCert.Meta.Numeral.peelCast? (e : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Peel one explicit cast wrapper when the head is a known cast constant.

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.Meta.Numeral.unsafeToRatByEval? (e : Lean.Expr) : Lean.MetaM (Option ℚ)

Last-resort extraction for closed expressions whose type is definitionally Rat. This is intentionally named so callers and CI audits can distinguish it from structural literal parsing.

Equations

• One or more equations did not get rendered due to their size.

partial def LeanCert.Meta.Numeral.toRat? (e : Lean.Expr) : Lean.MetaM (Option ℚ)

Attempt to parse a Lean expression as a rational constant.

partial def LeanCert.Meta.Numeral.toRat?.tryMatchNumeric (e : Lean.Expr) : Lean.MetaM (Option ℚ)

Try to match a numeric expression directly.

partial def LeanCert.Meta.Numeral.toRatLeaf? (e : Lean.Expr) : Lean.MetaM (Option ℚ)

Structural/literal rational extraction without arithmetic folding.

def LeanCert.Meta.Numeral.toRatFolded? (e : Lean.Expr) : Lean.MetaM (Option ℚ)

Rational extraction that may fold closed rational arithmetic.

Equations

• LeanCert.Meta.Numeral.toRatFolded? e = LeanCert.Meta.Numeral.toRat? e

def LeanCert.Meta.Numeral.toInt? (e : Lean.Expr) : Lean.MetaM (Option ℤ)

Attempt to parse a Lean expression as an integer constant.

Equations

• LeanCert.Meta.Numeral.toInt? e = do let __x ← LeanCert.Meta.Numeral.toRat? e match __x with | some q => if q.den = 1 then pure (some q.num) else pure none | x => pure none

def LeanCert.Meta.Numeral.toNat? (e : Lean.Expr) : Lean.MetaM (Option ℕ)

Attempt to parse a Lean expression as a natural-number constant.

Equations

• LeanCert.Meta.Numeral.toNat? e = do let __x ← LeanCert.Meta.Numeral.toInt? e match __x with | some z => if 0 ≤ z then pure (some z.toNat) else pure none | x => pure none

def LeanCert.Meta.Numeral.toRealRatNormalized? (e : Lean.Expr) : Lean.MetaM (Option ℚ)

Extract a rational after instantiating metavariables and normalizing reducible wrappers.

Equations

• One or more equations did not get rendered due to their size.