This module provides functions for evaluating simple `Nat` and `Int` expressions that appear in type classes (e.g., `ToInt` and `IsCharP`) used to configure `grind`. Using `whnf` for this purpose is too expensive and can exhaust the stack. We considered `evalExpr` as an alternative, but it introduces considerable overhead in files with many `grind` calls. We may still use `evalExpr` as a fallback in the future.

source
def Lean.Meta.Grind.Arith.evalNat? (e : Expr) :
GrindM (Option Nat)
Equations

- Lean.Meta.Grind.Arith.evalNat? e = (Lean.Meta.Grind.Arith.evalNatCore✝ e).run

Instances For

source
def Lean.Meta.Grind.Arith.evalInt? (e : Expr) :
GrindM (Option Int)
Equations

- Lean.Meta.Grind.Arith.evalInt? e = (Lean.Meta.Grind.Arith.evalIntCore✝ e).run

Instances For