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

@[inline]

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

@[inline]

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

def Int.reduceBinIntNatOp (name : Lean.Name) (op : Int → Nat → Int) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

@[inline]

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

@[inline]

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

def Int.reduceNeg : Lean.Meta.Simp.DSimproc

def Int.isPosValue : Lean.Meta.Simp.DSimproc

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

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

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

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

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

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

def Int.reduceTDiv : Lean.Meta.Simp.DSimproc

def Int.reduceTMod : Lean.Meta.Simp.DSimproc

def Int.reduceFDiv : Lean.Meta.Simp.DSimproc

def Int.reduceFMod : Lean.Meta.Simp.DSimproc

def Int.reduceBdiv : Lean.Meta.Simp.DSimproc

def Int.reduceBmod : Lean.Meta.Simp.DSimproc

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

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

def Int.reduceLE : Lean.Meta.Simp.Simproc

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

def Int.reduceGE : Lean.Meta.Simp.Simproc

def Int.reduceEq : Lean.Meta.Simp.Simproc

def Int.reduceNe : Lean.Meta.Simp.Simproc

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

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

@[inline]

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

def Int.reduceAbs : Lean.Meta.Simp.DSimproc

def Int.reduceToNat : Lean.Meta.Simp.DSimproc

def Int.reduceNegSucc : Lean.Meta.Simp.DSimproc

def Int.reduceOfNat : Lean.Meta.Simp.DSimproc

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

def Int.reduceNatCast : Lean.Meta.Simp.DSimproc

def Int.reduceNatCast' : Lean.Meta.Simp.DSimproc