Documentation

Lean.Meta.Tactic.Grind.Arith.FieldNormNum

source
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.

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