Functions for evaluating simple Nat and Int expressions that appear in type classes (e.g., ToInt and IsCharP). Using whnf for this purpose is too expensive and can exhaust the stack. We considered evalExpr as an alternative, but it introduces considerable overhead. We may use evalExpr as a fallback in the future.

def Lean.Meta.Sym.Arith.checkExp (k : Nat) : OptionT SymM Unit

Equations

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

def Lean.Meta.Sym.Arith.evalNat? (e : Expr) : SymM (Option Nat)

Equations

• Lean.Meta.Sym.Arith.evalNat? e = (Lean.Meta.Sym.Arith.evalNatCore✝ e).run

def Lean.Meta.Sym.Arith.evalInt? (e : Expr) : SymM (Option Int)

Equations

• Lean.Meta.Sym.Arith.evalInt? e = (Lean.Meta.Sym.Arith.evalIntCore✝ e).run