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.

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

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