def commandDeclare_uint_simprocs_ : Lean.ParserDescr

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

Equations

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

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

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

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

Equations

• UInt8.reduceGT = UInt8.reduceBinPred✝ `GT.gt 4 fun (x1 x2 : UInt8) => decide (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.reduceMul : Lean.Meta.Simp.DSimproc

Equations

• UInt8.reduceMul = UInt8.reduceBin✝ `HMul.hMul 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.reduceGE : Lean.Meta.Simp.Simproc

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

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

• UInt16.fromExpr e = do let __discr ← liftM (Lean.Meta.getOfNatValue? e `UInt16) match __discr with | some (n, snd) => pure (some (UInt16.ofNat n)) | x => pure none

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

Equations

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

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

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

Equations

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

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

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

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

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

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

Equations

• UInt16.reduceGT = UInt16.reduceBinPred✝ `GT.gt 4 fun (x1 x2 : UInt16) => 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.reduceMul : Lean.Meta.Simp.DSimproc

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

Equations

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

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

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

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

Equations

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

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

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

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

Equations

• UInt32.reduceLT = UInt32.reduceBinPred✝ `LT.lt 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.fromExpr : Lean.Expr → Lean.Meta.SimpM (Option UInt32)

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

Equations

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

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

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

Equations

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

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

Equations

• UInt64.reduceGT = UInt64.reduceBinPred✝ `GT.gt 4 fun (x1 x2 : UInt64) => decide (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.reduceGE : Lean.Meta.Simp.Simproc

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

Equations

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

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

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

def UInt64.reduceToNat : 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.reduceDiv : Lean.Meta.Simp.DSimproc

Equations

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

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

Equations

• UInt64.fromExpr e = do let __discr ← liftM (Lean.Meta.getOfNatValue? e `UInt64) match __discr with | some (n, snd) => pure (some (UInt64.ofNat n)) | x => pure none

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

Equations

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

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

Equations

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

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

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