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.

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

Attempt to parse a Lean expression as a rational constant.

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

Try to match a numeric expression directly.