def HexPolyZMathlib.PolyParse.evalRat (tactic : String) (e : Lean.Expr) : Lean.MetaM ℚ

Evaluate a closed Rat-typed (or ℚ) expression to a Rat at elaboration time. Rat is computable, so 2 ^ (-20), 1 / 1000, 10 ^ (-2) all reduce.

Equations

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

def HexPolyZMathlib.PolyParse.getNat (tactic : String) (e : Lean.Expr) : Lean.MetaM ℕ

Extract a Nat literal from an Expr (numerals and raw literals).

Equations

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

partial def HexPolyZMathlib.PolyParse.evalIntCoeff (tactic : String) (e : Lean.Expr) : Lean.MetaM ℤ

Interpret an integer scalar-coefficient leaf (OfNat, Neg, +, -, *, Int.ofNat, Nat.cast, Int.cast, raw literals). Throws the dedicated non-integer-coefficient error on anything else (e.g. a genuine ℚ/ℝ non-integer).

def HexPolyZMathlib.PolyParse.evalCoeff (tactic : String) (isRat : Bool) (e : Lean.Expr) : Lean.MetaM ℤ

Interpret a coefficient leaf of ring R. For ℚ (and ℤ), a leaf that is not structurally an integer is evaluated to a Rat and accepted only when its denominator is 1; otherwise the dedicated non-integer-coefficient error fires. For ℝ (not evaluable to Rat), only structurally integer leaves are accepted.

Equations

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

partial def HexPolyZMathlib.PolyParse.parsePoly (tactic : String) (isRat : Bool) (fuel : ℕ) (e : Lean.Expr) (onUnfold : Lean.Name → Lean.MetaM Unit := fun (x : Lean.Name) => pure ()) : Lean.MetaM Hex.ZPoly

Recursive interpreter from a Polynomial R expression over X / C / numerals (OfNat) / + / - / * / ^ (Nat) / neg, with named local defs unfolded one delta step at a time under a fuel guard, to a Hex.ZPoly value. isRat permits evaluating closed rational coefficients, provided they are integers. fuel bounds successive unfolding of named definitions. onUnfold records their names so that callers can unfold the same definitions when checking the result.