def Nat.fromExpr? (e : Lean.Expr) : Lean.Meta.SimpM (Option Nat)

@[inline]

def Nat.reduceUnary (declName : Lean.Name) (arity : Nat) (op : Nat → Nat) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

@[inline]

def Nat.reduceBin (declName : Lean.Name) (arity : Nat) (op : Nat → Nat → Nat) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

@[inline]

def Nat.reduceBinPred (declName : Lean.Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

@[inline]

def Nat.reduceBoolPred (declName : Lean.Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

def Nat.reduceSucc : Lean.Meta.Simp.DSimproc

def Nat.reduceAdd : Lean.Meta.Simp.DSimproc

def Nat.reduceMul : Lean.Meta.Simp.DSimproc

def Nat.reduceSub : Lean.Meta.Simp.DSimproc

def Nat.reduceDiv : Lean.Meta.Simp.DSimproc

def Nat.reduceMod : Lean.Meta.Simp.DSimproc

def Nat.reducePow : Lean.Meta.Simp.DSimproc

def Nat.reduceAnd : Lean.Meta.Simp.DSimproc

def Nat.reduceXor : Lean.Meta.Simp.DSimproc

def Nat.reduceOr : Lean.Meta.Simp.DSimproc

def Nat.reduceShiftLeft : Lean.Meta.Simp.DSimproc

def Nat.reduceShiftRight : Lean.Meta.Simp.DSimproc

def Nat.reduceGcd : Lean.Meta.Simp.DSimproc

def Nat.reduceLT : Lean.Meta.Simp.Simproc

def Nat.reduceGT : Lean.Meta.Simp.Simproc

def Nat.reduceBEq : Lean.Meta.Simp.DSimproc

def Nat.reduceBNe : Lean.Meta.Simp.DSimproc

def Nat.isValue : Lean.Meta.Simp.DSimproc

Return .done for Nat values. We don't want to unfold in the symbolic evaluator.

def Nat.applySimprocConst (expr : Lean.Expr) (nm : Lean.Name) (args : Array Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

inductive Nat.EqResult : Type

• decide (b : Bool) : EqResult
• false (p : Lean.Expr) : EqResult
• eq (x y p : Lean.Expr) : EqResult

def Nat.applyEqLemma (e : Lean.Expr → EqResult) (lemmaName : Lean.Name) (args : Array Lean.Expr) : Lean.Meta.SimpM (Option EqResult)

def Nat.reduceNatEqExpr (x y : Lean.Expr) : Lean.Meta.SimpM (Option EqResult)

def Nat.reduceEqDiff : Lean.Meta.Simp.Simproc

def Nat.reduceBeqDiff : Lean.Meta.Simp.Simproc

def Nat.reduceBneDiff : Lean.Meta.Simp.Simproc

def Nat.reduceLTLE (nm : Lean.Name) (arity : Nat) (isLT : Bool) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

def Nat.reduceLeDiff : Lean.Meta.Simp.Simproc

def Nat.reduceSubDiff : Lean.Meta.Simp.Simproc

def Nat.reduceDvd : Lean.Meta.Simp.Simproc