source
def commandDeclare_uint_simprocs_ :
Lean.ParserDescr
Equations

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

Instances For

source
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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For