Init.Data.UInt

source

@[extern lean_uint8_of_nat]

def UInt8.ofNat (n : Nat) :

UInt8

Equations

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

source

@[inline]

abbrev Nat.toUInt8 (n : Nat) :

UInt8

Equations

Nat.toUInt8 = UInt8.ofNat

source

@[extern lean_uint8_to_nat]

def UInt8.toNat (n : UInt8) :

Nat

Equations

UInt8.toNat n = n.val.val

source

@[extern lean_uint8_add]

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

UInt8

Equations

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

source

@[extern lean_uint8_sub]

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

UInt8

Equations

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

source

@[extern lean_uint8_mul]

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

UInt8

Equations

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

source

@[extern lean_uint8_div]

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

UInt8

Equations

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

source

@[extern lean_uint8_mod]

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

UInt8

Equations

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

source

@[extern lean_uint8_modn]

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

UInt8

Equations

UInt8.modn a n = { val := a.val % n }

source

@[extern lean_uint8_land]

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

UInt8

Equations

UInt8.land a b = { val := Fin.land a.val b.val }

source

@[extern lean_uint8_lor]

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

UInt8

Equations

UInt8.lor a b = { val := Fin.lor a.val b.val }

source

@[extern lean_uint8_xor]

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

UInt8

Equations

UInt8.xor a b = { val := Fin.xor a.val b.val }

source

@[extern lean_uint8_shift_left]

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

UInt8

Equations

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

source

@[extern lean_uint8_shift_right]

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

UInt8

Equations

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

source

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

Prop

Equations

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

source

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

Prop

Equations

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

source

instance instOfNatUInt8 {n : Nat} :

OfNat UInt8 n

Equations

instOfNatUInt8 = { ofNat := UInt8.ofNat n }

source

instance instAddUInt8 :

Add UInt8

Equations

instAddUInt8 = { add := UInt8.add }

source

instance instSubUInt8 :

Sub UInt8

Equations

instSubUInt8 = { sub := UInt8.sub }

source

instance instMulUInt8 :

Mul UInt8

Equations

instMulUInt8 = { mul := UInt8.mul }

source

instance instModUInt8 :

Mod UInt8

Equations

instModUInt8 = { mod := UInt8.mod }

source

instance instHModUInt8Nat :

HMod UInt8 Nat UInt8

Equations

instHModUInt8Nat = { hMod := UInt8.modn }

source

instance instDivUInt8 :

Div UInt8

Equations

instDivUInt8 = { div := UInt8.div }

source

instance instLTUInt8 :

LT UInt8

Equations

instLTUInt8 = { lt := UInt8.lt }

source

instance instLEUInt8 :

LE UInt8

Equations

instLEUInt8 = { le := UInt8.le }

source

@[extern lean_uint8_complement]

def UInt8.complement (a : UInt8) :

UInt8

Equations

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

source

instance instComplementUInt8 :

Complement UInt8

Equations

instComplementUInt8 = { complement := UInt8.complement }

source

instance instAndOpUInt8 :

AndOp UInt8

Equations

instAndOpUInt8 = { and := UInt8.land }

source

instance instOrOpUInt8 :

OrOp UInt8

Equations

instOrOpUInt8 = { or := UInt8.lor }

source

instance instXorUInt8 :

Xor UInt8

Equations

instXorUInt8 = { xor := UInt8.xor }

source

instance instShiftLeftUInt8 :

ShiftLeft UInt8

Equations

instShiftLeftUInt8 = { shiftLeft := UInt8.shiftLeft }

source

instance instShiftRightUInt8 :

ShiftRight UInt8

Equations

instShiftRightUInt8 = { shiftRight := UInt8.shiftRight }

source

@[extern lean_uint8_dec_lt]

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

Decidable (a < b)

Equations

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

source

@[extern lean_uint8_dec_le]

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

Decidable (a ≤ b)

Equations

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

source

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

Decidable (a < b)

Equations

instDecidableLtUInt8InstLTUInt8 a b = UInt8.decLt a b

source

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

Decidable (a ≤ b)

Equations

instDecidableLeUInt8InstLEUInt8 a b = UInt8.decLe a b

source

@[extern lean_uint16_of_nat]

def UInt16.ofNat (n : Nat) :

UInt16

Equations

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

source

@[inline]

abbrev Nat.toUInt16 (n : Nat) :

UInt16

Equations

Nat.toUInt16 = UInt16.ofNat

source

@[extern lean_uint16_to_nat]

def UInt16.toNat (n : UInt16) :

Nat

Equations

UInt16.toNat n = n.val.val

source

@[extern lean_uint16_add]

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

UInt16

Equations

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

source

@[extern lean_uint16_sub]

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

UInt16

Equations

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

source

@[extern lean_uint16_mul]

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

UInt16

Equations

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

source

@[extern lean_uint16_div]

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

UInt16

Equations

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

source

@[extern lean_uint16_mod]

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

UInt16

Equations

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

source

@[extern lean_uint16_modn]

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

UInt16

Equations

UInt16.modn a n = { val := a.val % n }

source

@[extern lean_uint16_land]

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

UInt16

Equations

UInt16.land a b = { val := Fin.land a.val b.val }

source

@[extern lean_uint16_lor]

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

UInt16

Equations

UInt16.lor a b = { val := Fin.lor a.val b.val }

source

@[extern lean_uint16_xor]

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

UInt16

Equations

UInt16.xor a b = { val := Fin.xor a.val b.val }

source

@[extern lean_uint16_shift_left]

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

UInt16

Equations

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

source

@[extern lean_uint16_to_uint8]

def UInt16.toUInt8 (a : UInt16) :

UInt8

Equations

UInt16.toUInt8 a = Nat.toUInt8 (UInt16.toNat a)

source

@[extern lean_uint8_to_uint16]

def UInt8.toUInt16 (a : UInt8) :

UInt16

Equations

UInt8.toUInt16 a = Nat.toUInt16 (UInt8.toNat a)

source

@[extern lean_uint16_shift_right]

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

UInt16

Equations

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

source

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

Prop

Equations

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

source

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

Prop

Equations

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

source

instance instOfNatUInt16 {n : Nat} :

OfNat UInt16 n

Equations

instOfNatUInt16 = { ofNat := UInt16.ofNat n }

source

instance instAddUInt16 :

Add UInt16

Equations

instAddUInt16 = { add := UInt16.add }

source

instance instSubUInt16 :

Sub UInt16

Equations

instSubUInt16 = { sub := UInt16.sub }

source

instance instMulUInt16 :

Mul UInt16

Equations

instMulUInt16 = { mul := UInt16.mul }

source

instance instModUInt16 :

Mod UInt16

Equations

instModUInt16 = { mod := UInt16.mod }

source

instance instHModUInt16Nat :

HMod UInt16 Nat UInt16

Equations

instHModUInt16Nat = { hMod := UInt16.modn }

source

instance instDivUInt16 :

Div UInt16

Equations

instDivUInt16 = { div := UInt16.div }

source

instance instLTUInt16 :

LT UInt16

Equations

instLTUInt16 = { lt := UInt16.lt }

source

instance instLEUInt16 :

LE UInt16

Equations

instLEUInt16 = { le := UInt16.le }

source

@[extern lean_uint16_complement]

def UInt16.complement (a : UInt16) :

UInt16

Equations

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

source

instance instComplementUInt16 :

Complement UInt16

Equations

instComplementUInt16 = { complement := UInt16.complement }

source

instance instAndOpUInt16 :

AndOp UInt16

Equations

instAndOpUInt16 = { and := UInt16.land }

source

instance instOrOpUInt16 :

OrOp UInt16

Equations

instOrOpUInt16 = { or := UInt16.lor }

source

instance instXorUInt16 :

Xor UInt16

Equations

instXorUInt16 = { xor := UInt16.xor }

source

instance instShiftLeftUInt16 :

ShiftLeft UInt16

Equations

instShiftLeftUInt16 = { shiftLeft := UInt16.shiftLeft }

source

instance instShiftRightUInt16 :

ShiftRight UInt16

Equations

instShiftRightUInt16 = { shiftRight := UInt16.shiftRight }

source

@[extern lean_uint16_dec_lt]

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

Decidable (a < b)

Equations

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

source

@[extern lean_uint16_dec_le]

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

Decidable (a ≤ b)

Equations

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

source

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

Decidable (a < b)

Equations

instDecidableLtUInt16InstLTUInt16 a b = UInt16.decLt a b

source

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

Decidable (a ≤ b)

Equations

instDecidableLeUInt16InstLEUInt16 a b = UInt16.decLe a b

source

@[extern lean_uint32_of_nat]

def UInt32.ofNat (n : Nat) :

UInt32

Equations

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

source

@[extern lean_uint32_of_nat]

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

UInt32

Equations

UInt32.ofNat' n h = { val := { val := n, isLt := h } }

source

@[inline]

abbrev Nat.toUInt32 (n : Nat) :

UInt32

Equations

Nat.toUInt32 = UInt32.ofNat

source

@[extern lean_uint32_add]

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

UInt32

Equations

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

source

@[extern lean_uint32_sub]

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

UInt32

Equations

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

source

@[extern lean_uint32_mul]

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

UInt32

Equations

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

source

@[extern lean_uint32_div]

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

UInt32

Equations

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

source

@[extern lean_uint32_mod]

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

UInt32

Equations

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

source

@[extern lean_uint32_modn]

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

UInt32

Equations

UInt32.modn a n = { val := a.val % n }

source

@[extern lean_uint32_land]

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

UInt32

Equations

UInt32.land a b = { val := Fin.land a.val b.val }

source

@[extern lean_uint32_lor]

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

UInt32

Equations

UInt32.lor a b = { val := Fin.lor a.val b.val }

source

@[extern lean_uint32_xor]

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

UInt32

Equations

UInt32.xor a b = { val := Fin.xor a.val b.val }

source

@[extern lean_uint32_shift_left]

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

UInt32

Equations

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

source

@[extern lean_uint32_shift_right]

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

UInt32

Equations

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

source

@[extern lean_uint32_to_uint8]

def UInt32.toUInt8 (a : UInt32) :

UInt8

Equations

UInt32.toUInt8 a = Nat.toUInt8 (UInt32.toNat a)

source

@[extern lean_uint32_to_uint16]

def UInt32.toUInt16 (a : UInt32) :

UInt16

Equations

UInt32.toUInt16 a = Nat.toUInt16 (UInt32.toNat a)

source

@[extern lean_uint8_to_uint32]

def UInt8.toUInt32 (a : UInt8) :

UInt32

Equations

UInt8.toUInt32 a = Nat.toUInt32 (UInt8.toNat a)

source

@[extern lean_uint16_to_uint32]

def UInt16.toUInt32 (a : UInt16) :

UInt32

Equations

UInt16.toUInt32 a = Nat.toUInt32 (UInt16.toNat a)

source

instance instOfNatUInt32 {n : Nat} :

OfNat UInt32 n

Equations

instOfNatUInt32 = { ofNat := UInt32.ofNat n }

source

instance instAddUInt32 :

Add UInt32

Equations

instAddUInt32 = { add := UInt32.add }

source

instance instSubUInt32 :

Sub UInt32

Equations

instSubUInt32 = { sub := UInt32.sub }

source

instance instMulUInt32 :

Mul UInt32

Equations

instMulUInt32 = { mul := UInt32.mul }

source

instance instModUInt32 :

Mod UInt32

Equations

instModUInt32 = { mod := UInt32.mod }

source

instance instHModUInt32Nat :

HMod UInt32 Nat UInt32

Equations

instHModUInt32Nat = { hMod := UInt32.modn }

source

instance instDivUInt32 :

Div UInt32

Equations

instDivUInt32 = { div := UInt32.div }

source

@[extern lean_uint32_complement]

def UInt32.complement (a : UInt32) :

UInt32

Equations

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

source

instance instComplementUInt32 :

Complement UInt32

Equations

instComplementUInt32 = { complement := UInt32.complement }

source

instance instAndOpUInt32 :

AndOp UInt32

Equations

instAndOpUInt32 = { and := UInt32.land }

source

instance instOrOpUInt32 :

OrOp UInt32

Equations

instOrOpUInt32 = { or := UInt32.lor }

source

instance instXorUInt32 :

Xor UInt32

Equations

instXorUInt32 = { xor := UInt32.xor }

source

instance instShiftLeftUInt32 :

ShiftLeft UInt32

Equations

instShiftLeftUInt32 = { shiftLeft := UInt32.shiftLeft }

source

instance instShiftRightUInt32 :

ShiftRight UInt32

Equations

instShiftRightUInt32 = { shiftRight := UInt32.shiftRight }

source

@[extern lean_uint64_of_nat]

def UInt64.ofNat (n : Nat) :

UInt64

Equations

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

source

@[inline]

abbrev Nat.toUInt64 (n : Nat) :

UInt64

Equations

Nat.toUInt64 = UInt64.ofNat

source

@[extern lean_uint64_to_nat]

def UInt64.toNat (n : UInt64) :

Nat

Equations

UInt64.toNat n = n.val.val

source

@[extern lean_uint64_add]

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

UInt64

Equations

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

source

@[extern lean_uint64_sub]

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

UInt64

Equations

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

source

@[extern lean_uint64_mul]

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

UInt64

Equations

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

source

@[extern lean_uint64_div]

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

UInt64

Equations

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

source

@[extern lean_uint64_mod]

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

UInt64

Equations

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

source

@[extern lean_uint64_modn]

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

UInt64

Equations

UInt64.modn a n = { val := a.val % n }

source

@[extern lean_uint64_land]

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

UInt64

Equations

UInt64.land a b = { val := Fin.land a.val b.val }

source

@[extern lean_uint64_lor]

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

UInt64

Equations

UInt64.lor a b = { val := Fin.lor a.val b.val }

source

@[extern lean_uint64_xor]

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

UInt64

Equations

UInt64.xor a b = { val := Fin.xor a.val b.val }

source

@[extern lean_uint64_shift_left]

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

UInt64

Equations

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

source

@[extern lean_uint64_shift_right]

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

UInt64

Equations

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

source

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

Prop

Equations

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

source

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

Prop

Equations

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

source

@[extern lean_uint64_to_uint8]

def UInt64.toUInt8 (a : UInt64) :

UInt8

Equations

UInt64.toUInt8 a = Nat.toUInt8 (UInt64.toNat a)

source

@[extern lean_uint64_to_uint16]

def UInt64.toUInt16 (a : UInt64) :

UInt16

Equations

UInt64.toUInt16 a = Nat.toUInt16 (UInt64.toNat a)

source

@[extern lean_uint64_to_uint32]

def UInt64.toUInt32 (a : UInt64) :

UInt32

Equations

UInt64.toUInt32 a = Nat.toUInt32 (UInt64.toNat a)

source

@[extern lean_uint8_to_uint64]

def UInt8.toUInt64 (a : UInt8) :

UInt64

Equations

UInt8.toUInt64 a = Nat.toUInt64 (UInt8.toNat a)

source

@[extern lean_uint16_to_uint64]

def UInt16.toUInt64 (a : UInt16) :

UInt64

Equations

UInt16.toUInt64 a = Nat.toUInt64 (UInt16.toNat a)

source

@[extern lean_uint32_to_uint64]

def UInt32.toUInt64 (a : UInt32) :

UInt64

Equations

UInt32.toUInt64 a = Nat.toUInt64 (UInt32.toNat a)

source

instance instOfNatUInt64 {n : Nat} :

OfNat UInt64 n

Equations

instOfNatUInt64 = { ofNat := UInt64.ofNat n }

source

instance instAddUInt64 :

Add UInt64

Equations

instAddUInt64 = { add := UInt64.add }

source

instance instSubUInt64 :

Sub UInt64

Equations

instSubUInt64 = { sub := UInt64.sub }

source

instance instMulUInt64 :

Mul UInt64

Equations

instMulUInt64 = { mul := UInt64.mul }

source

instance instModUInt64 :

Mod UInt64

Equations

instModUInt64 = { mod := UInt64.mod }

source

instance instHModUInt64Nat :

HMod UInt64 Nat UInt64

Equations

instHModUInt64Nat = { hMod := UInt64.modn }

source

instance instDivUInt64 :

Div UInt64

Equations

instDivUInt64 = { div := UInt64.div }

source

instance instLTUInt64 :

LT UInt64

Equations

instLTUInt64 = { lt := UInt64.lt }

source

instance instLEUInt64 :

LE UInt64

Equations

instLEUInt64 = { le := UInt64.le }

source

@[extern lean_uint64_complement]

def UInt64.complement (a : UInt64) :

UInt64

Equations

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

source

instance instComplementUInt64 :

Complement UInt64

Equations

instComplementUInt64 = { complement := UInt64.complement }

source

instance instAndOpUInt64 :

AndOp UInt64

Equations

instAndOpUInt64 = { and := UInt64.land }

source

instance instOrOpUInt64 :

OrOp UInt64

Equations

instOrOpUInt64 = { or := UInt64.lor }

source

instance instXorUInt64 :

Xor UInt64

Equations

instXorUInt64 = { xor := UInt64.xor }

source

instance instShiftLeftUInt64 :

ShiftLeft UInt64

Equations

instShiftLeftUInt64 = { shiftLeft := UInt64.shiftLeft }

source

instance instShiftRightUInt64 :

ShiftRight UInt64

Equations

instShiftRightUInt64 = { shiftRight := UInt64.shiftRight }

source

@[extern lean_bool_to_uint64]

def Bool.toUInt64 (b : Bool) :

UInt64

Equations

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

source

@[extern lean_uint64_dec_lt]

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

Decidable (a < b)

Equations

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

source

@[extern lean_uint64_dec_le]

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

Decidable (a ≤ b)

Equations

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

source

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

Decidable (a < b)

Equations

instDecidableLtUInt64InstLTUInt64 a b = UInt64.decLt a b

source

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

Decidable (a ≤ b)

Equations

instDecidableLeUInt64InstLEUInt64 a b = UInt64.decLe a b

source

theorem usize_size_gt_zero :

USize.size > 0

source

@[extern lean_usize_of_nat]

def USize.ofNat (n : Nat) :

USize

Equations

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

source

@[inline]

abbrev Nat.toUSize (n : Nat) :

USize

Equations

Nat.toUSize = USize.ofNat

source

@[extern lean_usize_to_nat]

def USize.toNat (n : USize) :

Nat

Equations

USize.toNat n = n.val.val

source

@[extern lean_usize_add]

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

USize

Equations

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

source

@[extern lean_usize_sub]

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

USize

Equations

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

source

@[extern lean_usize_mul]

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

USize

Equations

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

source

@[extern lean_usize_div]

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

USize

Equations

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

source

@[extern lean_usize_mod]

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

USize

Equations

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

source

@[extern lean_usize_modn]

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

USize

Equations

USize.modn a n = { val := a.val % n }

source

@[extern lean_usize_land]

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

USize

Equations

USize.land a b = { val := Fin.land a.val b.val }

source

@[extern lean_usize_lor]

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

USize

Equations

USize.lor a b = { val := Fin.lor a.val b.val }

source

@[extern lean_usize_xor]

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

USize

Equations

USize.xor a b = { val := Fin.xor a.val b.val }

source

@[extern lean_usize_shift_left]

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

USize

Equations

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

source

@[extern lean_usize_shift_right]

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

USize

Equations

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

source

@[extern lean_uint32_to_usize]

def UInt32.toUSize (a : UInt32) :

USize

Equations

UInt32.toUSize a = Nat.toUSize (UInt32.toNat a)

source

@[extern lean_usize_to_uint32]

def USize.toUInt32 (a : USize) :

UInt32

Equations

USize.toUInt32 a = Nat.toUInt32 (USize.toNat a)

source

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

Prop

Equations

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

source

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

Prop

Equations

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

source

instance instOfNatUSize {n : Nat} :

OfNat USize n

Equations

instOfNatUSize = { ofNat := USize.ofNat n }

source

instance instAddUSize :

Add USize

Equations

instAddUSize = { add := USize.add }

source

instance instSubUSize :

Sub USize

Equations

instSubUSize = { sub := USize.sub }

source

instance instMulUSize :

Mul USize

Equations

instMulUSize = { mul := USize.mul }

source

instance instModUSize :

Mod USize

Equations

instModUSize = { mod := USize.mod }

source

instance instHModUSizeNat :

HMod USize Nat USize

Equations

instHModUSizeNat = { hMod := USize.modn }

source

instance instDivUSize :

Div USize

Equations

instDivUSize = { div := USize.div }

source

instance instLTUSize :

LT USize

Equations

instLTUSize = { lt := USize.lt }

source

instance instLEUSize :

LE USize

Equations

instLEUSize = { le := USize.le }

source

@[extern lean_usize_complement]

def USize.complement (a : USize) :

USize

Equations

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

source

instance instComplementUSize :

Complement USize

Equations

instComplementUSize = { complement := USize.complement }

source

instance instAndOpUSize :

AndOp USize

Equations

instAndOpUSize = { and := USize.land }

source

instance instOrOpUSize :

OrOp USize

Equations

instOrOpUSize = { or := USize.lor }

source

instance instXorUSize :

Xor USize

Equations

instXorUSize = { xor := USize.xor }

source

instance instShiftLeftUSize :

ShiftLeft USize

Equations

instShiftLeftUSize = { shiftLeft := USize.shiftLeft }

source

instance instShiftRightUSize :

ShiftRight USize

Equations

instShiftRightUSize = { shiftRight := USize.shiftRight }

source

@[extern lean_usize_dec_lt]

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

Decidable (a < b)

Equations

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

source

@[extern lean_usize_dec_le]

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

Decidable (a ≤ b)

Equations

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

source

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

Decidable (a < b)

Equations

instDecidableLtUSizeInstLTUSize a b = USize.decLt a b

source

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

Decidable (a ≤ b)

Equations

instDecidableLeUSizeInstLEUSize a b = USize.decLe a b

source

theorem USize.modn_lt {m : Nat} (u : USize) :

m > 0 → USize.toNat (u % m) < m