def commandDeclare_uint_simprocs_ : Lean.ParserDescr

Equations

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

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

Equations

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

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

Equations

• UInt8.reduceGE = UInt8.reduceBinPred✝ `GE.ge 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.reduceAdd : Lean.Meta.Simp.DSimproc

Equations

• UInt8.reduceAdd = UInt8.reduceBin✝ `HAdd.hAdd 6 fun (x1 x2 : UInt8) => 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.reduceLT : Lean.Meta.Simp.Simproc

Equations

• UInt8.reduceLT = UInt8.reduceBinPred✝ `LT.lt 4 fun (x1 x2 : UInt8) => decide (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.reduceOfNatCore : Lean.Meta.Simp.DSimproc

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.reduceSub : Lean.Meta.Simp.DSimproc

Equations

• UInt8.reduceSub = UInt8.reduceBin✝ `HSub.hSub 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 UInt16.reduceOfNatCore : Lean.Meta.Simp.DSimproc

Equations

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

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

Equations

• UInt16.reduceDiv = UInt16.reduceBin✝ `HDiv.hDiv 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.reduceToNat : 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.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.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.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.reduceGT : Lean.Meta.Simp.Simproc

Equations

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

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

Equations

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

def UInt32.reduceOfNat : 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.reduceOfNatCore : Lean.Meta.Simp.DSimproc

Equations

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

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

Equations

• UInt32.reduceMod = UInt32.reduceBin✝ `HMod.hMod 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.fromExpr : Lean.Expr → Lean.Meta.SimpM (Option UInt32)

Equations

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

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

Equations

• UInt32.reduceSub = UInt32.reduceBin✝ `HSub.hSub 6 fun (x1 x2 : UInt32) => 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.reduceLE : Lean.Meta.Simp.Simproc

Equations

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

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

Equations

• UInt32.reduceLT = UInt32.reduceBinPred✝ `LT.lt 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 UInt32.reduceGE : Lean.Meta.Simp.Simproc

Equations

• UInt32.reduceGE = UInt32.reduceBinPred✝ `GE.ge 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 UInt64.reduceDiv : Lean.Meta.Simp.DSimproc

Equations

• UInt64.reduceDiv = UInt64.reduceBin✝ `HDiv.hDiv 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.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

Equations

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

def UInt64.reduceOfNatCore : 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.reduceLT : Lean.Meta.Simp.Simproc

Equations

• UInt64.reduceLT = UInt64.reduceBinPred✝ `LT.lt 4 fun (x1 x2 : UInt64) => decide (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.reduceSub : Lean.Meta.Simp.DSimproc

Equations

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

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.reduceMul : Lean.Meta.Simp.DSimproc

Equations

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

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

Equations

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