def Lean.Meta.Grind.Arith.evalFieldExpr? (e type : Expr) : MetaM (Option (Rat × Expr))

Evaluates the Field expression e with type type using the given exponential threshold, and returns some (v, h) s.t. h : e = ofRat v if successful.

Equations

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

def Lean.Meta.Grind.Arith.normFieldExpr? (e type : Expr) : MetaM (Option (Expr × Expr))

Equations

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