def Lean.commandDeclare_uint_simprocs_ : ParserDescr

Equations

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

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

Equations

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

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

Equations

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

def UInt8.reduceOr : Lean.Meta.Simp.DSimproc

Equations

• UInt8.reduceOr = UInt8.reduceBin✝ `HOr.hOr 6 fun (x1 x2 : UInt8) => x1 ||| x2

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def UInt8.reduceShiftRight : Lean.Meta.Simp.DSimproc

Equations

• UInt8.reduceShiftRight = UInt8.reduceBin✝ `HShiftRight.hShiftRight 6 fun (x1 x2 : UInt8) => x1 >>> x2

def UInt8.reduceXor : Lean.Meta.Simp.DSimproc

Equations

• UInt8.reduceXor = UInt8.reduceBin✝ `HXor.hXor 6 fun (x1 x2 : UInt8) => x1 ^^^ x2

def UInt8.reduceAnd : Lean.Meta.Simp.DSimproc

Equations

• UInt8.reduceAnd = UInt8.reduceBin✝ `HAnd.hAnd 6 fun (x1 x2 : UInt8) => x1 &&& x2

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

Equations

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

def UInt8.reduceOfNatLT : Lean.Meta.Simp.DSimproc

Equations

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

def UInt8.reduceShiftLeft : Lean.Meta.Simp.DSimproc

Equations

• UInt8.reduceShiftLeft = UInt8.reduceBin✝ `HShiftLeft.hShiftLeft 6 fun (x1 x2 : UInt8) => x1 <<< x2

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

Equations

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

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

Equations

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

def UInt8.reduceNot : Lean.Meta.Simp.DSimproc

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def UInt16.reduceAnd : Lean.Meta.Simp.DSimproc

Equations

• UInt16.reduceAnd = UInt16.reduceBin✝ `HAnd.hAnd 6 fun (x1 x2 : UInt16) => x1 &&& x2

def UInt16.reduceShiftLeft : Lean.Meta.Simp.DSimproc

Equations

• UInt16.reduceShiftLeft = UInt16.reduceBin✝ `HShiftLeft.hShiftLeft 6 fun (x1 x2 : UInt16) => x1 <<< x2

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def UInt16.reduceOfNatLT : Lean.Meta.Simp.DSimproc

Equations

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

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

Equations

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

def UInt16.reduceOr : Lean.Meta.Simp.DSimproc

Equations

• UInt16.reduceOr = UInt16.reduceBin✝ `HOr.hOr 6 fun (x1 x2 : UInt16) => x1 ||| x2

def UInt16.reduceNot : Lean.Meta.Simp.DSimproc

Equations

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

def UInt16.reduceXor : Lean.Meta.Simp.DSimproc

Equations

• UInt16.reduceXor = UInt16.reduceBin✝ `HXor.hXor 6 fun (x1 x2 : UInt16) => x1 ^^^ x2

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

Equations

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

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

Equations

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

def UInt16.reduceShiftRight : Lean.Meta.Simp.DSimproc

Equations

• UInt16.reduceShiftRight = UInt16.reduceBin✝ `HShiftRight.hShiftRight 6 fun (x1 x2 : UInt16) => x1 >>> x2

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

Equations

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

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

Equations

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

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

Equations

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

def UInt32.reduceOr : Lean.Meta.Simp.DSimproc

Equations

• UInt32.reduceOr = UInt32.reduceBin✝ `HOr.hOr 6 fun (x1 x2 : UInt32) => x1 ||| x2

def UInt32.reduceNot : Lean.Meta.Simp.DSimproc

Equations

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

def UInt32.reduceShiftRight : Lean.Meta.Simp.DSimproc

Equations

• UInt32.reduceShiftRight = UInt32.reduceBin✝ `HShiftRight.hShiftRight 6 fun (x1 x2 : UInt32) => x1 >>> x2

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

Equations

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

def UInt32.reduceShiftLeft : Lean.Meta.Simp.DSimproc

Equations

• UInt32.reduceShiftLeft = UInt32.reduceBin✝ `HShiftLeft.hShiftLeft 6 fun (x1 x2 : UInt32) => x1 <<< x2

def UInt32.reduceAnd : Lean.Meta.Simp.DSimproc

Equations

• UInt32.reduceAnd = UInt32.reduceBin✝ `HAnd.hAnd 6 fun (x1 x2 : UInt32) => x1 &&& x2

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

Equations

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

def UInt32.reduceXor : Lean.Meta.Simp.DSimproc

Equations

• UInt32.reduceXor = UInt32.reduceBin✝ `HXor.hXor 6 fun (x1 x2 : UInt32) => x1 ^^^ x2

def UInt32.reduceOfNatLT : Lean.Meta.Simp.DSimproc

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def UInt64.reduceShiftRight : Lean.Meta.Simp.DSimproc

Equations

• UInt64.reduceShiftRight = UInt64.reduceBin✝ `HShiftRight.hShiftRight 6 fun (x1 x2 : UInt64) => x1 >>> x2

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

Equations

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

def UInt64.reduceNot : Lean.Meta.Simp.DSimproc

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def UInt64.reduceShiftLeft : Lean.Meta.Simp.DSimproc

Equations

• UInt64.reduceShiftLeft = UInt64.reduceBin✝ `HShiftLeft.hShiftLeft 6 fun (x1 x2 : UInt64) => x1 <<< x2

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

Equations

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

def UInt64.reduceOr : Lean.Meta.Simp.DSimproc

Equations

• UInt64.reduceOr = UInt64.reduceBin✝ `HOr.hOr 6 fun (x1 x2 : UInt64) => x1 ||| x2

def UInt64.reduceOfNatLT : Lean.Meta.Simp.DSimproc

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def UInt64.reduceAnd : Lean.Meta.Simp.DSimproc

Equations

• UInt64.reduceAnd = UInt64.reduceBin✝ `HAnd.hAnd 6 fun (x1 x2 : UInt64) => x1 &&& x2

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

Equations

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

def UInt64.reduceXor : Lean.Meta.Simp.DSimproc

Equations

• UInt64.reduceXor = UInt64.reduceBin✝ `HXor.hXor 6 fun (x1 x2 : UInt64) => x1 ^^^ x2

def USize.reduceToNat : Lean.Meta.Simp.Simproc

Equations

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