@[extern lean_uint8_of_nat]
Equations
- UInt8.ofNat n = { val := Fin.ofNat n }
@[extern lean_uint8_to_nat]
Equations
- UInt8.toNat n = n.val.val
@[extern lean_uint8_modn]
Equations
- UInt8.modn a n = { val := a.val % n }
@[extern lean_uint8_land]
Equations
- UInt8.land a b = { val := Fin.land a.val b.val }
@[extern lean_uint8_shift_left]
Equations
- UInt8.shiftLeft a b = { val := a.val <<< (UInt8.modn b 8).val }
@[extern lean_uint8_shift_right]
Equations
- UInt8.shiftRight a b = { val := a.val >>> (UInt8.modn b 8).val }
Equations
- instOfNatUInt8 = { ofNat := UInt8.ofNat n }
Equations
- instHModUInt8Nat = { hMod := UInt8.modn }
@[extern lean_uint8_complement]
Equations
- UInt8.complement a = 0 - (a + 1)
Equations
- instComplementUInt8 = { complement := UInt8.complement }
Equations
- instShiftLeftUInt8 = { shiftLeft := UInt8.shiftLeft }
Equations
- instShiftRightUInt8 = { shiftRight := UInt8.shiftRight }
@[extern lean_uint8_dec_lt]
Equations
- UInt8.decLt a b = match a, b with | { val := n }, { val := m } => inferInstanceAs (Decidable (n < m))
@[extern lean_uint8_dec_le]
Equations
- UInt8.decLe a b = match a, b with | { val := n }, { val := m } => inferInstanceAs (Decidable (n ≤ m))
Equations
Equations
@[extern lean_uint16_of_nat]
Equations
- UInt16.ofNat n = { val := Fin.ofNat n }
@[extern lean_uint16_to_nat]
Equations
- UInt16.toNat n = n.val.val
@[extern lean_uint16_add]
Equations
- UInt16.add a b = { val := a.val + b.val }
@[extern lean_uint16_sub]
Equations
- UInt16.sub a b = { val := a.val - b.val }
@[extern lean_uint16_mul]
Equations
- UInt16.mul a b = { val := a.val * b.val }
@[extern lean_uint16_div]
Equations
- UInt16.div a b = { val := a.val / b.val }
@[extern lean_uint16_mod]
Equations
- UInt16.mod a b = { val := a.val % b.val }
@[extern lean_uint16_modn]
Equations
- UInt16.modn a n = { val := a.val % n }
@[extern lean_uint16_land]
Equations
- UInt16.land a b = { val := Fin.land a.val b.val }
@[extern lean_uint16_lor]
Equations
- UInt16.lor a b = { val := Fin.lor a.val b.val }
@[extern lean_uint16_xor]
Equations
- UInt16.xor a b = { val := Fin.xor a.val b.val }
@[extern lean_uint16_shift_left]
Equations
- UInt16.shiftLeft a b = { val := a.val <<< (UInt16.modn b 16).val }
@[extern lean_uint16_to_uint8]
Equations
@[extern lean_uint8_to_uint16]
Equations
@[extern lean_uint16_shift_right]
Equations
- UInt16.shiftRight a b = { val := a.val >>> (UInt16.modn b 16).val }
Equations
- instOfNatUInt16 = { ofNat := UInt16.ofNat n }
Equations
- instHModUInt16Nat = { hMod := UInt16.modn }
@[extern lean_uint16_complement]
Equations
- UInt16.complement a = 0 - (a + 1)
Equations
- instComplementUInt16 = { complement := UInt16.complement }
Equations
- instShiftLeftUInt16 = { shiftLeft := UInt16.shiftLeft }
Equations
- instShiftRightUInt16 = { shiftRight := UInt16.shiftRight }
@[extern lean_uint16_dec_lt]
Equations
- UInt16.decLt a b = match a, b with | { val := n }, { val := m } => inferInstanceAs (Decidable (n < m))
@[extern lean_uint16_dec_le]
Equations
- UInt16.decLe a b = match a, b with | { val := n }, { val := m } => inferInstanceAs (Decidable (n ≤ m))
Equations
Equations
@[extern lean_uint32_of_nat]
Equations
- UInt32.ofNat n = { val := Fin.ofNat n }
@[extern lean_uint32_of_nat]
Equations
- UInt32.ofNat' n h = { val := { val := n, isLt := h } }
@[extern lean_uint32_add]
Equations
- UInt32.add a b = { val := a.val + b.val }
@[extern lean_uint32_sub]
Equations
- UInt32.sub a b = { val := a.val - b.val }
@[extern lean_uint32_mul]
Equations
- UInt32.mul a b = { val := a.val * b.val }
@[extern lean_uint32_div]
Equations
- UInt32.div a b = { val := a.val / b.val }
@[extern lean_uint32_mod]
Equations
- UInt32.mod a b = { val := a.val % b.val }
@[extern lean_uint32_modn]
Equations
- UInt32.modn a n = { val := a.val % n }
@[extern lean_uint32_land]
Equations
- UInt32.land a b = { val := Fin.land a.val b.val }
@[extern lean_uint32_lor]
Equations
- UInt32.lor a b = { val := Fin.lor a.val b.val }
@[extern lean_uint32_xor]
Equations
- UInt32.xor a b = { val := Fin.xor a.val b.val }
@[extern lean_uint32_shift_left]
Equations
- UInt32.shiftLeft a b = { val := a.val <<< (UInt32.modn b 32).val }
@[extern lean_uint32_shift_right]
Equations
- UInt32.shiftRight a b = { val := a.val >>> (UInt32.modn b 32).val }
@[extern lean_uint32_to_uint8]
Equations
@[extern lean_uint32_to_uint16]
Equations
@[extern lean_uint8_to_uint32]
Equations
@[extern lean_uint16_to_uint32]
Equations
Equations
- instOfNatUInt32 = { ofNat := UInt32.ofNat n }
Equations
- instHModUInt32Nat = { hMod := UInt32.modn }
@[extern lean_uint32_complement]
Equations
- UInt32.complement a = 0 - (a + 1)
Equations
- instComplementUInt32 = { complement := UInt32.complement }
Equations
- instShiftLeftUInt32 = { shiftLeft := UInt32.shiftLeft }
Equations
- instShiftRightUInt32 = { shiftRight := UInt32.shiftRight }
@[extern lean_uint64_of_nat]
Equations
- UInt64.ofNat n = { val := Fin.ofNat n }
@[extern lean_uint64_to_nat]
Equations
- UInt64.toNat n = n.val.val
@[extern lean_uint64_add]
Equations
- UInt64.add a b = { val := a.val + b.val }
@[extern lean_uint64_sub]
Equations
- UInt64.sub a b = { val := a.val - b.val }
@[extern lean_uint64_mul]
Equations
- UInt64.mul a b = { val := a.val * b.val }
@[extern lean_uint64_div]
Equations
- UInt64.div a b = { val := a.val / b.val }
@[extern lean_uint64_mod]
Equations
- UInt64.mod a b = { val := a.val % b.val }
@[extern lean_uint64_modn]
Equations
- UInt64.modn a n = { val := a.val % n }
@[extern lean_uint64_land]
Equations
- UInt64.land a b = { val := Fin.land a.val b.val }
@[extern lean_uint64_lor]
Equations
- UInt64.lor a b = { val := Fin.lor a.val b.val }
@[extern lean_uint64_xor]
Equations
- UInt64.xor a b = { val := Fin.xor a.val b.val }
@[extern lean_uint64_shift_left]
Equations
- UInt64.shiftLeft a b = { val := a.val <<< (UInt64.modn b 64).val }
@[extern lean_uint64_shift_right]
Equations
- UInt64.shiftRight a b = { val := a.val >>> (UInt64.modn b 64).val }
@[extern lean_uint64_to_uint8]
Equations
@[extern lean_uint64_to_uint16]
Equations
@[extern lean_uint64_to_uint32]
Equations
@[extern lean_uint8_to_uint64]
Equations
@[extern lean_uint16_to_uint64]
Equations
@[extern lean_uint32_to_uint64]
Equations
Equations
- instOfNatUInt64 = { ofNat := UInt64.ofNat n }
Equations
- instHModUInt64Nat = { hMod := UInt64.modn }
@[extern lean_uint64_complement]
Equations
- UInt64.complement a = 0 - (a + 1)
Equations
- instComplementUInt64 = { complement := UInt64.complement }
Equations
- instShiftLeftUInt64 = { shiftLeft := UInt64.shiftLeft }
Equations
- instShiftRightUInt64 = { shiftRight := UInt64.shiftRight }
@[extern lean_bool_to_uint64]
Equations
- Bool.toUInt64 b = if b = true then 1 else 0
@[extern lean_uint64_dec_lt]
Equations
- UInt64.decLt a b = match a, b with | { val := n }, { val := m } => inferInstanceAs (Decidable (n < m))
@[extern lean_uint64_dec_le]
Equations
- UInt64.decLe a b = match a, b with | { val := n }, { val := m } => inferInstanceAs (Decidable (n ≤ m))
Equations
Equations
@[extern lean_usize_of_nat]
Equations
- USize.ofNat n = { val := Fin.ofNat' n usize_size_gt_zero }
@[extern lean_usize_to_nat]
Equations
- USize.toNat n = n.val.val
@[extern lean_usize_modn]
Equations
- USize.modn a n = { val := a.val % n }
@[extern lean_usize_land]
Equations
- USize.land a b = { val := Fin.land a.val b.val }
@[extern lean_usize_shift_left]
Equations
- USize.shiftLeft a b = { val := a.val <<< (USize.modn b System.Platform.numBits).val }
@[extern lean_usize_shift_right]
Equations
- USize.shiftRight a b = { val := a.val >>> (USize.modn b System.Platform.numBits).val }
@[extern lean_uint32_to_usize]
Equations
@[extern lean_usize_to_uint32]
Equations
Equations
- instOfNatUSize = { ofNat := USize.ofNat n }
Equations
- instHModUSizeNat = { hMod := USize.modn }
@[extern lean_usize_complement]
Equations
- USize.complement a = 0 - (a + 1)
Equations
- instComplementUSize = { complement := USize.complement }
Equations
- instShiftLeftUSize = { shiftLeft := USize.shiftLeft }
Equations
- instShiftRightUSize = { shiftRight := USize.shiftRight }
@[extern lean_usize_dec_lt]
Equations
- USize.decLt a b = match a, b with | { val := n }, { val := m } => inferInstanceAs (Decidable (n < m))
@[extern lean_usize_dec_le]
Equations
- USize.decLe a b = match a, b with | { val := n }, { val := m } => inferInstanceAs (Decidable (n ≤ m))