@[extern lean_uint8_of_nat]

def UInt8.ofNat (n : Nat) : UInt8

@[inline, reducible]

abbrev Nat.toUInt8 (n : Nat) : UInt8

@[extern lean_uint8_to_nat]

def UInt8.toNat (n : UInt8) : Nat

@[extern lean_uint8_add]

def UInt8.add (a : UInt8) (b : UInt8) : UInt8

@[extern lean_uint8_sub]

def UInt8.sub (a : UInt8) (b : UInt8) : UInt8

@[extern lean_uint8_mul]

def UInt8.mul (a : UInt8) (b : UInt8) : UInt8

@[extern lean_uint8_div]

def UInt8.div (a : UInt8) (b : UInt8) : UInt8

@[extern lean_uint8_mod]

def UInt8.mod (a : UInt8) (b : UInt8) : UInt8

@[extern lean_uint8_modn]

def UInt8.modn (a : UInt8) (n : Nat) : UInt8

@[extern lean_uint8_land]

def UInt8.land (a : UInt8) (b : UInt8) : UInt8

@[extern lean_uint8_lor]

def UInt8.lor (a : UInt8) (b : UInt8) : UInt8

@[extern lean_uint8_xor]

def UInt8.xor (a : UInt8) (b : UInt8) : UInt8

@[extern lean_uint8_shift_left]

def UInt8.shiftLeft (a : UInt8) (b : UInt8) : UInt8

@[extern lean_uint8_shift_right]

def UInt8.shiftRight (a : UInt8) (b : UInt8) : UInt8

def UInt8.lt (a : UInt8) (b : UInt8) : Prop

def UInt8.le (a : UInt8) (b : UInt8) : Prop

instance instOfNatUInt8 {n : Nat} : OfNat UInt8 n

instance instAddUInt8 : Add UInt8

instance instSubUInt8 : Sub UInt8

instance instMulUInt8 : Mul UInt8

instance instModUInt8 : Mod UInt8

instance instHModUInt8Nat : HMod UInt8 Nat UInt8

instance instDivUInt8 : Div UInt8

instance instLTUInt8 : LT UInt8

instance instLEUInt8 : LE UInt8

@[extern lean_uint8_complement]

def UInt8.complement (a : UInt8) : UInt8

instance instComplementUInt8 : Complement UInt8

instance instAndOpUInt8 : AndOp UInt8

instance instOrOpUInt8 : OrOp UInt8

instance instXorUInt8 : Xor UInt8

instance instShiftLeftUInt8 : ShiftLeft UInt8

instance instShiftRightUInt8 : ShiftRight UInt8

@[extern lean_uint8_dec_lt]

def UInt8.decLt (a : UInt8) (b : UInt8) : Decidable (a < b)

@[extern lean_uint8_dec_le]

def UInt8.decLe (a : UInt8) (b : UInt8) : Decidable (a ≤ b)

instance instDecidableLtUInt8InstLTUInt8 (a : UInt8) (b : UInt8) : Decidable (a < b)

instance instDecidableLeUInt8InstLEUInt8 (a : UInt8) (b : UInt8) : Decidable (a ≤ b)

instance instMaxUInt8 : Max UInt8

instance instMinUInt8 : Min UInt8

@[extern lean_uint16_of_nat]

def UInt16.ofNat (n : Nat) : UInt16

@[inline, reducible]

abbrev Nat.toUInt16 (n : Nat) : UInt16

@[extern lean_uint16_to_nat]

def UInt16.toNat (n : UInt16) : Nat

@[extern lean_uint16_add]

def UInt16.add (a : UInt16) (b : UInt16) : UInt16

@[extern lean_uint16_sub]

def UInt16.sub (a : UInt16) (b : UInt16) : UInt16

@[extern lean_uint16_mul]

def UInt16.mul (a : UInt16) (b : UInt16) : UInt16

@[extern lean_uint16_div]

def UInt16.div (a : UInt16) (b : UInt16) : UInt16

@[extern lean_uint16_mod]

def UInt16.mod (a : UInt16) (b : UInt16) : UInt16

@[extern lean_uint16_modn]

def UInt16.modn (a : UInt16) (n : Nat) : UInt16

@[extern lean_uint16_land]

def UInt16.land (a : UInt16) (b : UInt16) : UInt16

@[extern lean_uint16_lor]

def UInt16.lor (a : UInt16) (b : UInt16) : UInt16

@[extern lean_uint16_xor]

def UInt16.xor (a : UInt16) (b : UInt16) : UInt16

@[extern lean_uint16_shift_left]

def UInt16.shiftLeft (a : UInt16) (b : UInt16) : UInt16

@[extern lean_uint16_to_uint8]

def UInt16.toUInt8 (a : UInt16) : UInt8

@[extern lean_uint8_to_uint16]

def UInt8.toUInt16 (a : UInt8) : UInt16

@[extern lean_uint16_shift_right]

def UInt16.shiftRight (a : UInt16) (b : UInt16) : UInt16

def UInt16.lt (a : UInt16) (b : UInt16) : Prop

def UInt16.le (a : UInt16) (b : UInt16) : Prop

instance instOfNatUInt16 {n : Nat} : OfNat UInt16 n

instance instAddUInt16 : Add UInt16

instance instSubUInt16 : Sub UInt16

instance instMulUInt16 : Mul UInt16

instance instModUInt16 : Mod UInt16

instance instHModUInt16Nat : HMod UInt16 Nat UInt16

instance instDivUInt16 : Div UInt16

instance instLTUInt16 : LT UInt16

instance instLEUInt16 : LE UInt16

@[extern lean_uint16_complement]

def UInt16.complement (a : UInt16) : UInt16

instance instComplementUInt16 : Complement UInt16

instance instAndOpUInt16 : AndOp UInt16

instance instOrOpUInt16 : OrOp UInt16

instance instXorUInt16 : Xor UInt16

instance instShiftLeftUInt16 : ShiftLeft UInt16

instance instShiftRightUInt16 : ShiftRight UInt16

@[extern lean_uint16_dec_lt]

def UInt16.decLt (a : UInt16) (b : UInt16) : Decidable (a < b)

@[extern lean_uint16_dec_le]

def UInt16.decLe (a : UInt16) (b : UInt16) : Decidable (a ≤ b)

instance instDecidableLtUInt16InstLTUInt16 (a : UInt16) (b : UInt16) : Decidable (a < b)

instance instDecidableLeUInt16InstLEUInt16 (a : UInt16) (b : UInt16) : Decidable (a ≤ b)

instance instMaxUInt16 : Max UInt16

instance instMinUInt16 : Min UInt16

@[extern lean_uint32_of_nat]

def UInt32.ofNat (n : Nat) : UInt32

@[extern lean_uint32_of_nat]

def UInt32.ofNat' (n : Nat) (h : n < UInt32.size) : UInt32

@[inline, reducible]

abbrev Nat.toUInt32 (n : Nat) : UInt32

@[extern lean_uint32_add]

def UInt32.add (a : UInt32) (b : UInt32) : UInt32

@[extern lean_uint32_sub]

def UInt32.sub (a : UInt32) (b : UInt32) : UInt32

@[extern lean_uint32_mul]

def UInt32.mul (a : UInt32) (b : UInt32) : UInt32

@[extern lean_uint32_div]

def UInt32.div (a : UInt32) (b : UInt32) : UInt32

@[extern lean_uint32_mod]

def UInt32.mod (a : UInt32) (b : UInt32) : UInt32

@[extern lean_uint32_modn]

def UInt32.modn (a : UInt32) (n : Nat) : UInt32

@[extern lean_uint32_land]

def UInt32.land (a : UInt32) (b : UInt32) : UInt32

@[extern lean_uint32_lor]

def UInt32.lor (a : UInt32) (b : UInt32) : UInt32

@[extern lean_uint32_xor]

def UInt32.xor (a : UInt32) (b : UInt32) : UInt32

@[extern lean_uint32_shift_left]

def UInt32.shiftLeft (a : UInt32) (b : UInt32) : UInt32

@[extern lean_uint32_shift_right]

def UInt32.shiftRight (a : UInt32) (b : UInt32) : UInt32

@[extern lean_uint32_to_uint8]

def UInt32.toUInt8 (a : UInt32) : UInt8

@[extern lean_uint32_to_uint16]

def UInt32.toUInt16 (a : UInt32) : UInt16

@[extern lean_uint8_to_uint32]

def UInt8.toUInt32 (a : UInt8) : UInt32

@[extern lean_uint16_to_uint32]

def UInt16.toUInt32 (a : UInt16) : UInt32

instance instOfNatUInt32 {n : Nat} : OfNat UInt32 n

instance instAddUInt32 : Add UInt32

instance instSubUInt32 : Sub UInt32

instance instMulUInt32 : Mul UInt32

instance instModUInt32 : Mod UInt32

instance instHModUInt32Nat : HMod UInt32 Nat UInt32

instance instDivUInt32 : Div UInt32

@[extern lean_uint32_complement]

def UInt32.complement (a : UInt32) : UInt32

instance instComplementUInt32 : Complement UInt32

instance instAndOpUInt32 : AndOp UInt32

instance instOrOpUInt32 : OrOp UInt32

instance instXorUInt32 : Xor UInt32

instance instShiftLeftUInt32 : ShiftLeft UInt32

instance instShiftRightUInt32 : ShiftRight UInt32

@[extern lean_uint64_of_nat]

def UInt64.ofNat (n : Nat) : UInt64

@[inline, reducible]

abbrev Nat.toUInt64 (n : Nat) : UInt64

@[extern lean_uint64_to_nat]

def UInt64.toNat (n : UInt64) : Nat

@[extern lean_uint64_add]

def UInt64.add (a : UInt64) (b : UInt64) : UInt64

@[extern lean_uint64_sub]

def UInt64.sub (a : UInt64) (b : UInt64) : UInt64

@[extern lean_uint64_mul]

def UInt64.mul (a : UInt64) (b : UInt64) : UInt64

@[extern lean_uint64_div]

def UInt64.div (a : UInt64) (b : UInt64) : UInt64

@[extern lean_uint64_mod]

def UInt64.mod (a : UInt64) (b : UInt64) : UInt64

@[extern lean_uint64_modn]

def UInt64.modn (a : UInt64) (n : Nat) : UInt64

@[extern lean_uint64_land]

def UInt64.land (a : UInt64) (b : UInt64) : UInt64

@[extern lean_uint64_lor]

def UInt64.lor (a : UInt64) (b : UInt64) : UInt64

@[extern lean_uint64_xor]

def UInt64.xor (a : UInt64) (b : UInt64) : UInt64

@[extern lean_uint64_shift_left]

def UInt64.shiftLeft (a : UInt64) (b : UInt64) : UInt64

@[extern lean_uint64_shift_right]

def UInt64.shiftRight (a : UInt64) (b : UInt64) : UInt64

def UInt64.lt (a : UInt64) (b : UInt64) : Prop

def UInt64.le (a : UInt64) (b : UInt64) : Prop

@[extern lean_uint64_to_uint8]

def UInt64.toUInt8 (a : UInt64) : UInt8

@[extern lean_uint64_to_uint16]

def UInt64.toUInt16 (a : UInt64) : UInt16

@[extern lean_uint64_to_uint32]

def UInt64.toUInt32 (a : UInt64) : UInt32

@[extern lean_uint8_to_uint64]

def UInt8.toUInt64 (a : UInt8) : UInt64

@[extern lean_uint16_to_uint64]

def UInt16.toUInt64 (a : UInt16) : UInt64

@[extern lean_uint32_to_uint64]

def UInt32.toUInt64 (a : UInt32) : UInt64

instance instOfNatUInt64 {n : Nat} : OfNat UInt64 n

instance instAddUInt64 : Add UInt64

instance instSubUInt64 : Sub UInt64

instance instMulUInt64 : Mul UInt64

instance instModUInt64 : Mod UInt64

instance instHModUInt64Nat : HMod UInt64 Nat UInt64

instance instDivUInt64 : Div UInt64

instance instLTUInt64 : LT UInt64

instance instLEUInt64 : LE UInt64

@[extern lean_uint64_complement]

def UInt64.complement (a : UInt64) : UInt64

instance instComplementUInt64 : Complement UInt64

instance instAndOpUInt64 : AndOp UInt64

instance instOrOpUInt64 : OrOp UInt64

instance instXorUInt64 : Xor UInt64

instance instShiftLeftUInt64 : ShiftLeft UInt64

instance instShiftRightUInt64 : ShiftRight UInt64

@[extern lean_bool_to_uint64]

def Bool.toUInt64 (b : Bool) : UInt64

@[extern lean_uint64_dec_lt]

def UInt64.decLt (a : UInt64) (b : UInt64) : Decidable (a < b)

@[extern lean_uint64_dec_le]

def UInt64.decLe (a : UInt64) (b : UInt64) : Decidable (a ≤ b)

instance instDecidableLtUInt64InstLTUInt64 (a : UInt64) (b : UInt64) : Decidable (a < b)

instance instDecidableLeUInt64InstLEUInt64 (a : UInt64) (b : UInt64) : Decidable (a ≤ b)

instance instMaxUInt64 : Max UInt64

instance instMinUInt64 : Min UInt64

theorem usize_size_gt_zero : USize.size > 0

@[extern lean_usize_of_nat]

def USize.ofNat (n : Nat) : USize

@[inline, reducible]

abbrev Nat.toUSize (n : Nat) : USize

@[extern lean_usize_to_nat]

def USize.toNat (n : USize) : Nat

@[extern lean_usize_add]

def USize.add (a : USize) (b : USize) : USize

@[extern lean_usize_sub]

def USize.sub (a : USize) (b : USize) : USize

@[extern lean_usize_mul]

def USize.mul (a : USize) (b : USize) : USize

@[extern lean_usize_div]

def USize.div (a : USize) (b : USize) : USize

@[extern lean_usize_mod]

def USize.mod (a : USize) (b : USize) : USize

@[extern lean_usize_modn]

def USize.modn (a : USize) (n : Nat) : USize

@[extern lean_usize_land]

def USize.land (a : USize) (b : USize) : USize

@[extern lean_usize_lor]

def USize.lor (a : USize) (b : USize) : USize

@[extern lean_usize_xor]

def USize.xor (a : USize) (b : USize) : USize

@[extern lean_usize_shift_left]

def USize.shiftLeft (a : USize) (b : USize) : USize

@[extern lean_usize_shift_right]

def USize.shiftRight (a : USize) (b : USize) : USize

@[extern lean_uint32_to_usize]

def UInt32.toUSize (a : UInt32) : USize

@[extern lean_usize_to_uint32]

def USize.toUInt32 (a : USize) : UInt32

def USize.lt (a : USize) (b : USize) : Prop

def USize.le (a : USize) (b : USize) : Prop

instance instOfNatUSize {n : Nat} : OfNat USize n

instance instAddUSize : Add USize

instance instSubUSize : Sub USize

instance instMulUSize : Mul USize

instance instModUSize : Mod USize

instance instHModUSizeNat : HMod USize Nat USize

instance instDivUSize : Div USize

instance instLTUSize : LT USize

instance instLEUSize : LE USize

@[extern lean_usize_complement]

def USize.complement (a : USize) : USize

instance instComplementUSize : Complement USize

instance instAndOpUSize : AndOp USize

instance instOrOpUSize : OrOp USize

instance instXorUSize : Xor USize

instance instShiftLeftUSize : ShiftLeft USize

instance instShiftRightUSize : ShiftRight USize

@[extern lean_usize_dec_lt]

def USize.decLt (a : USize) (b : USize) : Decidable (a < b)

@[extern lean_usize_dec_le]

def USize.decLe (a : USize) (b : USize) : Decidable (a ≤ b)

instance instDecidableLtUSizeInstLTUSize (a : USize) (b : USize) : Decidable (a < b)

instance instDecidableLeUSizeInstLEUSize (a : USize) (b : USize) : Decidable (a ≤ b)

instance instMaxUSize : Max USize

instance instMinUSize : Min USize

theorem USize.modn_lt {m : Nat} (u : USize) : m > 0 → USize.toNat (u % m) < m