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

Equations

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

def Int.toExpr (v : Int) : Lean.Expr

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Int.reduceSub = Int.reduceBin `HSub.hSub 6 fun (x x_1 : Int) => x - x_1

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

Equations

• Int.reduceDiv = Int.reduceBin `HDiv.hDiv 6 fun (x x_1 : Int) => x / x_1

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

Equations

• Int.reduceMod = Int.reduceBin `HMod.hMod 6 fun (x x_1 : Int) => x % x_1

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Int.reduceGE = Int.reduceBinPred `GE.ge 4 fun (x x_1 : Int) => decide (x ≥ x_1)