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

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

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