def commandDeclare_uint_simprocs_ : Lean.ParserDescr

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def UInt8.toExpr : UInt8.Value✝ → Lean.Expr

Equations

• UInt8.toExpr v = let vExpr := Lean.mkRawNatLit (UInt8.Value.value✝ v).val.val; Lean.mkApp2 (UInt8.Value.ofNatFn✝ v) vExpr (Lean.mkApp (Lean.mkConst `UInt8.instOfNat) vExpr)

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

Equations

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

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

Equations

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

def UInt8.fromExpr : Lean.Expr → OptionT Lean.Meta.SimpM UInt8.Value✝

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def UInt16.toExpr : UInt16.Value✝ → Lean.Expr

Equations

• UInt16.toExpr v = let vExpr := Lean.mkRawNatLit (UInt16.Value.value✝ v).val.val; Lean.mkApp2 (UInt16.Value.ofNatFn✝ v) vExpr (Lean.mkApp (Lean.mkConst `UInt16.instOfNat) vExpr)

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def UInt16.fromExpr : Lean.Expr → OptionT Lean.Meta.SimpM UInt16.Value✝

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def UInt32.toExpr : UInt32.Value✝ → Lean.Expr

Equations

• UInt32.toExpr v = let vExpr := Lean.mkRawNatLit (UInt32.Value.value✝ v).val.val; Lean.mkApp2 (UInt32.Value.ofNatFn✝ v) vExpr (Lean.mkApp (Lean.mkConst `UInt32.instOfNat) vExpr)

def UInt32.fromExpr : Lean.Expr → OptionT Lean.Meta.SimpM UInt32.Value✝

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 (x x_1 : UInt32) => decide (x < x_1)

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def UInt64.fromExpr : Lean.Expr → OptionT Lean.Meta.SimpM UInt64.Value✝

Equations

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

def UInt64.toExpr : UInt64.Value✝ → Lean.Expr

Equations

• UInt64.toExpr v = let vExpr := Lean.mkRawNatLit (UInt64.Value.value✝ v).val.val; Lean.mkApp2 (UInt64.Value.ofNatFn✝ v) vExpr (Lean.mkApp (Lean.mkConst `UInt64.instOfNat) vExpr)

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• USize.reduceAdd = USize.reduceBin✝ `HAdd.hAdd 6 fun (x x_1 : USize) => x + x_1

def USize.toExpr : USize.Value✝ → Lean.Expr

Equations

• USize.toExpr v = let vExpr := Lean.mkRawNatLit (USize.Value.value✝ v).val.val; Lean.mkApp2 (USize.Value.ofNatFn✝ v) vExpr (Lean.mkApp (Lean.mkConst `USize.instOfNat) vExpr)

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

Equations

• USize.reduceMod = USize.reduceBin✝ `HMod.hMod 6 fun (x x_1 : USize) => x % x_1

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

Equations

• USize.reduceGE = USize.reduceBinPred✝ `GE.ge 4 fun (x x_1 : USize) => decide (x ≥ x_1)

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

Equations

• USize.reduceLT = USize.reduceBinPred✝ `LT.lt 4 fun (x x_1 : USize) => decide (x < x_1)

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

Equations

• USize.reduceSub = USize.reduceBin✝ `HSub.hSub 6 fun (x x_1 : USize) => x - x_1

def USize.fromExpr : Lean.Expr → OptionT Lean.Meta.SimpM USize.Value✝

Equations

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

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

Equations

• USize.reduceMul = USize.reduceBin✝ `HMul.hMul 6 fun (x x_1 : USize) => x * x_1

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

Equations

• USize.reduceGT = USize.reduceBinPred✝ `GT.gt 4 fun (x x_1 : USize) => decide (x > x_1)

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

Equations

• USize.reduceDiv = USize.reduceBin✝ `HDiv.hDiv 6 fun (x x_1 : USize) => x / x_1

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

Equations

• USize.reduceLE = USize.reduceBinPred✝ `LE.le 4 fun (x x_1 : USize) => decide (x ≤ x_1)