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

Equations

• Int.fromExpr? e = liftM (Lean.Meta.getIntValue? e)

@[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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Int.reduceAdd = Int.reduceBin `HAdd.hAdd 6 fun (x1 x2 : Int) => x1 + x2

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

Equations

• Int.reduceMul = Int.reduceBin `HMul.hMul 6 fun (x1 x2 : Int) => x1 * x2

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

Equations

• Int.reduceTMod = Int.reduceBin `Int.mod 2 Int.tmod

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

Equations

• Int.reduceFDiv = Int.reduceBin `Int.fdiv 2 Int.fdiv

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

Equations

• Int.reduceFMod = Int.reduceBin `Int.fmod 2 Int.fmod

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

Equations

• Int.reduceBdiv = Int.reduceBinIntNatOp `Int.bdiv Int.bdiv

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

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

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

Equations

• Int.reduceLT = Int.reduceBinPred `LT.lt 4 fun (x1 x2 : Int) => decide (x1 < x2)

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

Equations

• Int.reduceLE = Int.reduceBinPred `LE.le 4 fun (x1 x2 : Int) => decide (x1 ≤ x2)

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

Equations

• Int.reduceGT = Int.reduceBinPred `GT.gt 4 fun (x1 x2 : Int) => decide (x1 > x2)

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

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

Equations

• Int.reduceEq = Int.reduceBinPred `Eq 3 fun (x1 x2 : Int) => decide (x1 = x2)

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

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

Equations

• Int.reduceBEq = Int.reduceBoolPred `BEq.beq 4 fun (x1 x2 : Int) => x1 == x2

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

Equations

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

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

Equations

• Int.reduceAbs = Int.reduceNatCore `Int.natAbs Int.natAbs

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

Equations

• Int.reduceToNat = Int.reduceNatCore `Int.toNat Int.toNat

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

Equations

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

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

Equations

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