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.

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