def commandDeclare_sint_simprocs_ : Lean.ParserDescr

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Int8.reduceMod = Int8.reduceBin✝ `HMod.hMod 6 fun (x1 x2 : Int8) => x1 % x2

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

Equations

• Int8.reduceSub = Int8.reduceBin✝ `HSub.hSub 6 fun (x1 x2 : Int8) => x1 - x2

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

Equations

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

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

Equations

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

def Int8.reduceOfInt : Lean.Meta.Simp.DSimproc

Equations

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

def Int8.reduceToInt : Lean.Meta.Simp.DSimproc

Equations

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

def Int8.fromExpr : Lean.Expr → Lean.Meta.SimpM (Option Int8)

Equations

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

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

Equations

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

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

Equations

• Int8.reduceDiv = Int8.reduceBin✝ `HDiv.hDiv 6 fun (x1 x2 : Int8) => x1 / x2

def Int8.reduceOfIntLE : Lean.Meta.Simp.DSimproc

Equations

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

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

Equations

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

def Int8.reduceToNatClampNeg : Lean.Meta.Simp.DSimproc

Equations

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

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

Equations

• Int8.reduceGE = Int8.reduceBinPred✝ `GE.ge 4 fun (x1 x2 : Int8) => decide (x1 ≥ x2)

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

Equations

• Int16.reduceDiv = Int16.reduceBin✝ `HDiv.hDiv 6 fun (x1 x2 : Int16) => x1 / x2

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

Equations

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

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

Equations

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

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

Equations

• Int16.reduceSub = Int16.reduceBin✝ `HSub.hSub 6 fun (x1 x2 : Int16) => x1 - x2

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

Equations

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

def Int16.fromExpr : Lean.Expr → Lean.Meta.SimpM (Option Int16)

Equations

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

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

Equations

• Int16.reduceGE = Int16.reduceBinPred✝ `GE.ge 4 fun (x1 x2 : Int16) => decide (x1 ≥ x2)

def Int16.reduceToNatClampNeg : Lean.Meta.Simp.DSimproc

Equations

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

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

Equations

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

def Int16.reduceToInt : Lean.Meta.Simp.DSimproc

Equations

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

def Int16.reduceOfIntLE : Lean.Meta.Simp.DSimproc

Equations

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

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

Equations

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

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

Equations

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

def Int16.reduceOfInt : Lean.Meta.Simp.DSimproc

Equations

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

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

Equations

• Int16.reduceMod = Int16.reduceBin✝ `HMod.hMod 6 fun (x1 x2 : Int16) => x1 % x2

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

Equations

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

def Int32.reduceToNatClampNeg : Lean.Meta.Simp.DSimproc

Equations

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

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

Equations

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

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

Equations

• Int32.reduceSub = Int32.reduceBin✝ `HSub.hSub 6 fun (x1 x2 : Int32) => x1 - x2

def Int32.reduceOfIntLE : Lean.Meta.Simp.DSimproc

Equations

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

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

Equations

• Int32.reduceDiv = Int32.reduceBin✝ `HDiv.hDiv 6 fun (x1 x2 : Int32) => x1 / x2

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

Equations

• Int32.reduceGE = Int32.reduceBinPred✝ `GE.ge 4 fun (x1 x2 : Int32) => decide (x1 ≥ x2)

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

Equations

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

def Int32.fromExpr : Lean.Expr → Lean.Meta.SimpM (Option Int32)

Equations

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

def Int32.reduceOfInt : Lean.Meta.Simp.DSimproc

Equations

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

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

Equations

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

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

Equations

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

def Int32.reduceToInt : Lean.Meta.Simp.DSimproc

Equations

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

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

Equations

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

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

Equations

• Int32.reduceMod = Int32.reduceBin✝ `HMod.hMod 6 fun (x1 x2 : Int32) => x1 % x2

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

Equations

• Int64.reduceDiv = Int64.reduceBin✝ `HDiv.hDiv 6 fun (x1 x2 : Int64) => x1 / x2

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

Equations

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

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

Equations

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

def Int64.reduceToNatClampNeg : Lean.Meta.Simp.DSimproc

Equations

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

def Int64.reduceOfIntLE : Lean.Meta.Simp.DSimproc

Equations

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

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

Equations

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

def Int64.reduceToInt : Lean.Meta.Simp.DSimproc

Equations

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

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

Equations

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

def Int64.fromExpr : Lean.Expr → Lean.Meta.SimpM (Option Int64)

Equations

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

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

Equations

• Int64.reduceGE = Int64.reduceBinPred✝ `GE.ge 4 fun (x1 x2 : Int64) => decide (x1 ≥ x2)

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

Equations

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

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

Equations

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

def Int64.reduceOfInt : Lean.Meta.Simp.DSimproc

Equations

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

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

Equations

• Int64.reduceMod = Int64.reduceBin✝ `HMod.hMod 6 fun (x1 x2 : Int64) => x1 % x2

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

Equations

• Int64.reduceSub = Int64.reduceBin✝ `HSub.hSub 6 fun (x1 x2 : Int64) => x1 - x2

def ISize.reduceToNatClampNeg : Lean.Meta.Simp.Simproc

Equations

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

def ISize.reduceToInt : Lean.Meta.Simp.Simproc

Equations

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