@[extern lean_uint8_of_nat]

def UInt8.ofNat (n : Nat) : UInt8

Equations

• UInt8.ofNat n = { val := Fin.ofNat n }

@[reducible, inline]

abbrev Nat.toUInt8 (n : Nat) : UInt8

Equations

• Nat.toUInt8 = UInt8.ofNat

@[extern lean_uint8_to_nat]

def UInt8.toNat (n : UInt8) : Nat

Equations

• n.toNat = ↑n.val

@[extern lean_uint8_add]

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

Equations

• a.add b = { val := a.val + b.val }

@[extern lean_uint8_sub]

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

Equations

• a.sub b = { val := a.val - b.val }

@[extern lean_uint8_mul]

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

Equations

• a.mul b = { val := a.val * b.val }

@[extern lean_uint8_div]

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

Equations

• a.div b = { val := a.val / b.val }

@[extern lean_uint8_mod]

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

Equations

• a.mod b = { val := a.val % b.val }

@[extern lean_uint8_modn]

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

Equations

• a.modn n = { val := a.val.modn n }

@[extern lean_uint8_land]

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

Equations

• a.land b = { val := a.val.land b.val }

@[extern lean_uint8_lor]

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

Equations

• a.lor b = { val := a.val.lor b.val }

@[extern lean_uint8_xor]

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

Equations

• a.xor b = { val := a.val.xor b.val }

@[extern lean_uint8_shift_left]

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

Equations

• a.shiftLeft b = { val := a.val <<< (b.modn 8).val }

@[extern lean_uint8_shift_right]

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

Equations

• a.shiftRight b = { val := a.val >>> (b.modn 8).val }

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

Equations

• a.lt b = (a.val < b.val)

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

Equations

• a.le b = (a.val ≤ b.val)

instance UInt8.instOfNat {n : Nat} : OfNat UInt8 n

Equations

• UInt8.instOfNat = { ofNat := UInt8.ofNat n }

instance instAddUInt8 : Add UInt8

Equations

• instAddUInt8 = { add := UInt8.add }

instance instSubUInt8 : Sub UInt8

Equations

• instSubUInt8 = { sub := UInt8.sub }

instance instMulUInt8 : Mul UInt8

Equations

• instMulUInt8 = { mul := UInt8.mul }

instance instModUInt8 : Mod UInt8

Equations

• instModUInt8 = { mod := UInt8.mod }

instance instHModUInt8Nat : HMod UInt8 Nat UInt8

Equations

• instHModUInt8Nat = { hMod := UInt8.modn }

instance instDivUInt8 : Div UInt8

Equations

• instDivUInt8 = { div := UInt8.div }

instance instLTUInt8 : LT UInt8

Equations

• instLTUInt8 = { lt := UInt8.lt }

instance instLEUInt8 : LE UInt8

Equations

• instLEUInt8 = { le := UInt8.le }

@[extern lean_uint8_complement]

def UInt8.complement (a : UInt8) : UInt8

Equations

• a.complement = 0 - (a + 1)

instance instComplementUInt8 : Complement UInt8

Equations

• instComplementUInt8 = { complement := UInt8.complement }

instance instAndOpUInt8 : AndOp UInt8

Equations

• instAndOpUInt8 = { and := UInt8.land }

instance instOrOpUInt8 : OrOp UInt8

Equations

• instOrOpUInt8 = { or := UInt8.lor }

instance instXorUInt8 : Xor UInt8

Equations

• instXorUInt8 = { xor := UInt8.xor }

instance instShiftLeftUInt8 : ShiftLeft UInt8

Equations

• instShiftLeftUInt8 = { shiftLeft := UInt8.shiftLeft }

instance instShiftRightUInt8 : ShiftRight UInt8

Equations

• instShiftRightUInt8 = { shiftRight := UInt8.shiftRight }

@[extern lean_uint8_dec_lt]

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

Equations

• a.decLt b = match a, b with | { val := n }, { val := m } => inferInstanceAs (Decidable (n < m))

@[extern lean_uint8_dec_le]

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

Equations

• a.decLe b = match a, b with | { val := n }, { val := m } => inferInstanceAs (Decidable (n ≤ m))

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

Equations

• instDecidableLtUInt8 a b = a.decLt b

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

Equations

• instDecidableLeUInt8 a b = a.decLe b

instance instMaxUInt8 : Max UInt8

Equations

• instMaxUInt8 = maxOfLe

instance instMinUInt8 : Min UInt8

Equations

• instMinUInt8 = minOfLe

@[extern lean_uint16_of_nat]

def UInt16.ofNat (n : Nat) : UInt16

Equations

• UInt16.ofNat n = { val := Fin.ofNat n }

@[reducible, inline]

abbrev Nat.toUInt16 (n : Nat) : UInt16

Equations

• Nat.toUInt16 = UInt16.ofNat

@[extern lean_uint16_to_nat]

def UInt16.toNat (n : UInt16) : Nat

Equations

• n.toNat = ↑n.val

@[extern lean_uint16_add]

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

Equations

• a.add b = { val := a.val + b.val }

@[extern lean_uint16_sub]

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

Equations

• a.sub b = { val := a.val - b.val }

@[extern lean_uint16_mul]

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

Equations

• a.mul b = { val := a.val * b.val }

@[extern lean_uint16_div]

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

Equations

• a.div b = { val := a.val / b.val }

@[extern lean_uint16_mod]

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

Equations

• a.mod b = { val := a.val % b.val }

@[extern lean_uint16_modn]

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

Equations

• a.modn n = { val := a.val.modn n }

@[extern lean_uint16_land]

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

Equations

• a.land b = { val := a.val.land b.val }

@[extern lean_uint16_lor]

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

Equations

• a.lor b = { val := a.val.lor b.val }

@[extern lean_uint16_xor]

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

Equations

• a.xor b = { val := a.val.xor b.val }

@[extern lean_uint16_shift_left]

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

Equations

• a.shiftLeft b = { val := a.val <<< (b.modn 16).val }

@[extern lean_uint16_to_uint8]

def UInt16.toUInt8 (a : UInt16) : UInt8

Equations

• a.toUInt8 = a.toNat.toUInt8

@[extern lean_uint8_to_uint16]

def UInt8.toUInt16 (a : UInt8) : UInt16

Equations

• a.toUInt16 = { val := ⟨↑a.val, ⋯⟩ }

@[extern lean_uint16_shift_right]

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

Equations

• a.shiftRight b = { val := a.val >>> (b.modn 16).val }

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

Equations

• a.lt b = (a.val < b.val)

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

Equations

• a.le b = (a.val ≤ b.val)

instance UInt16.instOfNat {n : Nat} : OfNat UInt16 n

Equations

• UInt16.instOfNat = { ofNat := UInt16.ofNat n }

instance instAddUInt16 : Add UInt16

Equations

• instAddUInt16 = { add := UInt16.add }

instance instSubUInt16 : Sub UInt16

Equations

• instSubUInt16 = { sub := UInt16.sub }

instance instMulUInt16 : Mul UInt16

Equations

• instMulUInt16 = { mul := UInt16.mul }

instance instModUInt16 : Mod UInt16

Equations

• instModUInt16 = { mod := UInt16.mod }

instance instHModUInt16Nat : HMod UInt16 Nat UInt16

Equations

• instHModUInt16Nat = { hMod := UInt16.modn }

instance instDivUInt16 : Div UInt16

Equations

• instDivUInt16 = { div := UInt16.div }

instance instLTUInt16 : LT UInt16

Equations

• instLTUInt16 = { lt := UInt16.lt }

instance instLEUInt16 : LE UInt16

Equations

• instLEUInt16 = { le := UInt16.le }

@[extern lean_uint16_complement]

def UInt16.complement (a : UInt16) : UInt16

Equations

• a.complement = 0 - (a + 1)

instance instComplementUInt16 : Complement UInt16

Equations

• instComplementUInt16 = { complement := UInt16.complement }

instance instAndOpUInt16 : AndOp UInt16

Equations

• instAndOpUInt16 = { and := UInt16.land }

instance instOrOpUInt16 : OrOp UInt16

Equations

• instOrOpUInt16 = { or := UInt16.lor }

instance instXorUInt16 : Xor UInt16

Equations

• instXorUInt16 = { xor := UInt16.xor }

instance instShiftLeftUInt16 : ShiftLeft UInt16

Equations

• instShiftLeftUInt16 = { shiftLeft := UInt16.shiftLeft }

instance instShiftRightUInt16 : ShiftRight UInt16

Equations

• instShiftRightUInt16 = { shiftRight := UInt16.shiftRight }

@[extern lean_uint16_dec_lt]

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

Equations

• a.decLt b = match a, b with | { val := n }, { val := m } => inferInstanceAs (Decidable (n < m))

@[extern lean_uint16_dec_le]

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

Equations

• a.decLe b = match a, b with | { val := n }, { val := m } => inferInstanceAs (Decidable (n ≤ m))

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

Equations

• instDecidableLtUInt16 a b = a.decLt b

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

Equations

• instDecidableLeUInt16 a b = a.decLe b

instance instMaxUInt16 : Max UInt16

Equations

• instMaxUInt16 = maxOfLe

instance instMinUInt16 : Min UInt16

Equations

• instMinUInt16 = minOfLe

@[extern lean_uint32_of_nat]

def UInt32.ofNat (n : Nat) : UInt32

Equations

• UInt32.ofNat n = { val := Fin.ofNat n }

@[extern lean_uint32_of_nat]

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

Equations

• UInt32.ofNat' n h = { val := ⟨n, h⟩ }

def UInt32.ofNatTruncate (n : Nat) : UInt32

Converts the given natural number to UInt32, but returns 2^32 - 1 for natural numbers >= 2^32.

Equations

• UInt32.ofNatTruncate n = if h : n < UInt32.size then UInt32.ofNat' n h else UInt32.ofNat' (UInt32.size - 1) UInt32.ofNatTruncate.proof_1

@[reducible, inline]

abbrev Nat.toUInt32 (n : Nat) : UInt32

Equations

• Nat.toUInt32 = UInt32.ofNat

@[extern lean_uint32_add]

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

Equations

• a.add b = { val := a.val + b.val }

@[extern lean_uint32_sub]

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

Equations

• a.sub b = { val := a.val - b.val }

@[extern lean_uint32_mul]

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

Equations

• a.mul b = { val := a.val * b.val }

@[extern lean_uint32_div]

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

Equations

• a.div b = { val := a.val / b.val }

@[extern lean_uint32_mod]

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

Equations

• a.mod b = { val := a.val % b.val }

@[extern lean_uint32_modn]

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

Equations

• a.modn n = { val := a.val.modn n }

@[extern lean_uint32_land]

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

Equations

• a.land b = { val := a.val.land b.val }

@[extern lean_uint32_lor]

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

Equations

• a.lor b = { val := a.val.lor b.val }

@[extern lean_uint32_xor]

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

Equations

• a.xor b = { val := a.val.xor b.val }

@[extern lean_uint32_shift_left]

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

Equations

• a.shiftLeft b = { val := a.val <<< (b.modn 32).val }

@[extern lean_uint32_shift_right]

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

Equations

• a.shiftRight b = { val := a.val >>> (b.modn 32).val }

@[extern lean_uint32_to_uint8]

def UInt32.toUInt8 (a : UInt32) : UInt8

Equations

• a.toUInt8 = a.toNat.toUInt8

@[extern lean_uint32_to_uint16]

def UInt32.toUInt16 (a : UInt32) : UInt16

Equations

• a.toUInt16 = a.toNat.toUInt16

@[extern lean_uint8_to_uint32]

def UInt8.toUInt32 (a : UInt8) : UInt32

Equations

• a.toUInt32 = { val := ⟨↑a.val, ⋯⟩ }

@[extern lean_uint16_to_uint32]

def UInt16.toUInt32 (a : UInt16) : UInt32

Equations

• a.toUInt32 = { val := ⟨↑a.val, ⋯⟩ }

instance UInt32.instOfNat {n : Nat} : OfNat UInt32 n

Equations

• UInt32.instOfNat = { ofNat := UInt32.ofNat n }

instance instAddUInt32 : Add UInt32

Equations

• instAddUInt32 = { add := UInt32.add }

instance instSubUInt32 : Sub UInt32

Equations

• instSubUInt32 = { sub := UInt32.sub }

instance instMulUInt32 : Mul UInt32

Equations

• instMulUInt32 = { mul := UInt32.mul }

instance instModUInt32 : Mod UInt32

Equations

• instModUInt32 = { mod := UInt32.mod }

instance instHModUInt32Nat : HMod UInt32 Nat UInt32

Equations

• instHModUInt32Nat = { hMod := UInt32.modn }

instance instDivUInt32 : Div UInt32

Equations

• instDivUInt32 = { div := UInt32.div }

@[extern lean_uint32_complement]

def UInt32.complement (a : UInt32) : UInt32

Equations

• a.complement = 0 - (a + 1)

instance instComplementUInt32 : Complement UInt32

Equations

• instComplementUInt32 = { complement := UInt32.complement }

instance instAndOpUInt32 : AndOp UInt32

Equations

• instAndOpUInt32 = { and := UInt32.land }

instance instOrOpUInt32 : OrOp UInt32

Equations

• instOrOpUInt32 = { or := UInt32.lor }

instance instXorUInt32 : Xor UInt32

Equations

• instXorUInt32 = { xor := UInt32.xor }

instance instShiftLeftUInt32 : ShiftLeft UInt32

Equations

• instShiftLeftUInt32 = { shiftLeft := UInt32.shiftLeft }

instance instShiftRightUInt32 : ShiftRight UInt32

Equations

• instShiftRightUInt32 = { shiftRight := UInt32.shiftRight }

@[extern lean_uint64_of_nat]

def UInt64.ofNat (n : Nat) : UInt64

Equations

• UInt64.ofNat n = { val := Fin.ofNat n }

@[reducible, inline]

abbrev Nat.toUInt64 (n : Nat) : UInt64

Equations

• Nat.toUInt64 = UInt64.ofNat

@[extern lean_uint64_to_nat]

def UInt64.toNat (n : UInt64) : Nat

Equations

• n.toNat = ↑n.val

@[extern lean_uint64_add]

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

Equations

• a.add b = { val := a.val + b.val }

@[extern lean_uint64_sub]

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

Equations

• a.sub b = { val := a.val - b.val }

@[extern lean_uint64_mul]

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

Equations

• a.mul b = { val := a.val * b.val }

@[extern lean_uint64_div]

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

Equations

• a.div b = { val := a.val / b.val }

@[extern lean_uint64_mod]

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

Equations

• a.mod b = { val := a.val % b.val }

@[extern lean_uint64_modn]

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

Equations

• a.modn n = { val := a.val.modn n }

@[extern lean_uint64_land]

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

Equations

• a.land b = { val := a.val.land b.val }

@[extern lean_uint64_lor]

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

Equations

• a.lor b = { val := a.val.lor b.val }

@[extern lean_uint64_xor]

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

Equations

• a.xor b = { val := a.val.xor b.val }

@[extern lean_uint64_shift_left]

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

Equations

• a.shiftLeft b = { val := a.val <<< (b.modn 64).val }

@[extern lean_uint64_shift_right]

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

Equations

• a.shiftRight b = { val := a.val >>> (b.modn 64).val }

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

Equations

• a.lt b = (a.val < b.val)

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

Equations

• a.le b = (a.val ≤ b.val)

@[extern lean_uint64_to_uint8]

def UInt64.toUInt8 (a : UInt64) : UInt8

Equations

• a.toUInt8 = a.toNat.toUInt8

@[extern lean_uint64_to_uint16]

def UInt64.toUInt16 (a : UInt64) : UInt16

Equations

• a.toUInt16 = a.toNat.toUInt16

@[extern lean_uint64_to_uint32]

def UInt64.toUInt32 (a : UInt64) : UInt32

Equations

• a.toUInt32 = a.toNat.toUInt32

@[extern lean_uint8_to_uint64]

def UInt8.toUInt64 (a : UInt8) : UInt64

Equations

• a.toUInt64 = { val := ⟨↑a.val, ⋯⟩ }

@[extern lean_uint16_to_uint64]

def UInt16.toUInt64 (a : UInt16) : UInt64

Equations

• a.toUInt64 = { val := ⟨↑a.val, ⋯⟩ }

@[extern lean_uint32_to_uint64]

def UInt32.toUInt64 (a : UInt32) : UInt64

Equations

• a.toUInt64 = { val := ⟨↑a.val, ⋯⟩ }

instance UInt64.instOfNat {n : Nat} : OfNat UInt64 n

Equations

• UInt64.instOfNat = { ofNat := UInt64.ofNat n }

instance instAddUInt64 : Add UInt64

Equations

• instAddUInt64 = { add := UInt64.add }

instance instSubUInt64 : Sub UInt64

Equations

• instSubUInt64 = { sub := UInt64.sub }

instance instMulUInt64 : Mul UInt64

Equations

• instMulUInt64 = { mul := UInt64.mul }

instance instModUInt64 : Mod UInt64

Equations

• instModUInt64 = { mod := UInt64.mod }

instance instHModUInt64Nat : HMod UInt64 Nat UInt64

Equations

• instHModUInt64Nat = { hMod := UInt64.modn }

instance instDivUInt64 : Div UInt64

Equations

• instDivUInt64 = { div := UInt64.div }

instance instLTUInt64 : LT UInt64

Equations

• instLTUInt64 = { lt := UInt64.lt }

instance instLEUInt64 : LE UInt64

Equations

• instLEUInt64 = { le := UInt64.le }

@[extern lean_uint64_complement]

def UInt64.complement (a : UInt64) : UInt64

Equations

• a.complement = 0 - (a + 1)

instance instComplementUInt64 : Complement UInt64

Equations

• instComplementUInt64 = { complement := UInt64.complement }

instance instAndOpUInt64 : AndOp UInt64

Equations

• instAndOpUInt64 = { and := UInt64.land }

instance instOrOpUInt64 : OrOp UInt64

Equations

• instOrOpUInt64 = { or := UInt64.lor }

instance instXorUInt64 : Xor UInt64

Equations

• instXorUInt64 = { xor := UInt64.xor }

instance instShiftLeftUInt64 : ShiftLeft UInt64

Equations

• instShiftLeftUInt64 = { shiftLeft := UInt64.shiftLeft }

instance instShiftRightUInt64 : ShiftRight UInt64

Equations

• instShiftRightUInt64 = { shiftRight := UInt64.shiftRight }

@[extern lean_bool_to_uint64]

def Bool.toUInt64 (b : Bool) : UInt64

Equations

• b.toUInt64 = if b = true then 1 else 0

@[extern lean_uint64_dec_lt]

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

Equations

• a.decLt b = match a, b with | { val := n }, { val := m } => inferInstanceAs (Decidable (n < m))

@[extern lean_uint64_dec_le]

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

Equations

• a.decLe b = match a, b with | { val := n }, { val := m } => inferInstanceAs (Decidable (n ≤ m))

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

Equations

• instDecidableLtUInt64 a b = a.decLt b

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

Equations

• instDecidableLeUInt64 a b = a.decLe b

instance instMaxUInt64 : Max UInt64

Equations

• instMaxUInt64 = maxOfLe

instance instMinUInt64 : Min UInt64

Equations

• instMinUInt64 = minOfLe

theorem usize_size_gt_zero : USize.size > 0

@[extern lean_usize_of_nat]

def USize.ofNat (n : Nat) : USize

Equations

• USize.ofNat n = { val := Fin.ofNat' n usize_size_gt_zero }

@[reducible, inline]

abbrev Nat.toUSize (n : Nat) : USize

Equations

• Nat.toUSize = USize.ofNat

@[extern lean_usize_to_nat]

def USize.toNat (n : USize) : Nat

Equations

• n.toNat = ↑n.val

@[extern lean_usize_add]

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

Equations

• a.add b = { val := a.val + b.val }

@[extern lean_usize_sub]

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

Equations

• a.sub b = { val := a.val - b.val }

@[extern lean_usize_mul]

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

Equations

• a.mul b = { val := a.val * b.val }

@[extern lean_usize_div]

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

Equations

• a.div b = { val := a.val / b.val }

@[extern lean_usize_mod]

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

Equations

• a.mod b = { val := a.val % b.val }

@[extern lean_usize_modn]

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

Equations

• a.modn n = { val := a.val.modn n }

@[extern lean_usize_land]

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

Equations

• a.land b = { val := a.val.land b.val }

@[extern lean_usize_lor]

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

Equations

• a.lor b = { val := a.val.lor b.val }

@[extern lean_usize_xor]

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

Equations

• a.xor b = { val := a.val.xor b.val }

@[extern lean_usize_shift_left]

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

Equations

• a.shiftLeft b = { val := a.val <<< (b.modn System.Platform.numBits).val }

@[extern lean_usize_shift_right]

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

Equations

• a.shiftRight b = { val := a.val >>> (b.modn System.Platform.numBits).val }

@[extern lean_uint32_to_usize]

def UInt32.toUSize (a : UInt32) : USize

Equations

• a.toUSize = USize.ofNat32 ↑a.val ⋯

@[extern lean_usize_to_uint32]

def USize.toUInt32 (a : USize) : UInt32

Equations

• a.toUInt32 = a.toNat.toUInt32

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

Equations

• a.lt b = (a.val < b.val)

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

Equations

• a.le b = (a.val ≤ b.val)

instance USize.instOfNat {n : Nat} : OfNat USize n

Equations

• USize.instOfNat = { ofNat := USize.ofNat n }

instance instAddUSize : Add USize

Equations

• instAddUSize = { add := USize.add }

instance instSubUSize : Sub USize

Equations

• instSubUSize = { sub := USize.sub }

instance instMulUSize : Mul USize

Equations

• instMulUSize = { mul := USize.mul }

instance instModUSize : Mod USize

Equations

• instModUSize = { mod := USize.mod }

instance instHModUSizeNat : HMod USize Nat USize

Equations

• instHModUSizeNat = { hMod := USize.modn }

instance instDivUSize : Div USize

Equations

• instDivUSize = { div := USize.div }

instance instLTUSize : LT USize

Equations

• instLTUSize = { lt := USize.lt }

instance instLEUSize : LE USize

Equations

• instLEUSize = { le := USize.le }

@[extern lean_usize_complement]

def USize.complement (a : USize) : USize

Equations

• a.complement = 0 - (a + 1)

instance instComplementUSize : Complement USize

Equations

• instComplementUSize = { complement := USize.complement }

instance instAndOpUSize : AndOp USize

Equations

• instAndOpUSize = { and := USize.land }

instance instOrOpUSize : OrOp USize

Equations

• instOrOpUSize = { or := USize.lor }

instance instXorUSize : Xor USize

Equations

• instXorUSize = { xor := USize.xor }

instance instShiftLeftUSize : ShiftLeft USize

Equations

• instShiftLeftUSize = { shiftLeft := USize.shiftLeft }

instance instShiftRightUSize : ShiftRight USize

Equations

• instShiftRightUSize = { shiftRight := USize.shiftRight }

@[extern lean_usize_dec_lt]

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

Equations

• a.decLt b = match a, b with | { val := n }, { val := m } => inferInstanceAs (Decidable (n < m))

@[extern lean_usize_dec_le]

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

Equations

• a.decLe b = match a, b with | { val := n }, { val := m } => inferInstanceAs (Decidable (n ≤ m))

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

Equations

• instDecidableLtUSize a b = a.decLt b

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

Equations

• instDecidableLeUSize a b = a.decLe b

instance instMaxUSize : Max USize

Equations

• instMaxUSize = maxOfLe

instance instMinUSize : Min USize

Equations

• instMinUSize = minOfLe

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