def commandDeclare_uint_theorems_ : Lean.ParserDescr

Equations

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

theorem UInt8.sub_def (a : UInt8) (b : UInt8) : a - b = { toBitVec := a.toBitVec - b.toBitVec }

@[simp]

theorem UInt8.not_le {a : UInt8} {b : UInt8} : ¬a ≤ b ↔ b < a

theorem UInt8.toBitVec_eq_of_lt {a : Nat} : a < UInt8.size → (UInt8.ofNat a).toBitVec.toNat = a

instance UInt8.instInhabited : Inhabited UInt8

Equations

• UInt8.instInhabited = { default := 0 }

@[simp]

theorem UInt8.lt_irrefl (a : UInt8) : ¬a < a

theorem UInt8.ne_of_lt {a : UInt8} {b : UInt8} (h : a < b) : a ≠ b

@[simp]

theorem UInt8.toBitVec_ofNat (n : Nat) : (OfNat.ofNat n).toBitVec = BitVec.ofNat 8 n

theorem UInt8.add_def (a : UInt8) (b : UInt8) : a + b = { toBitVec := a.toBitVec + b.toBitVec }

theorem UInt8.toNat_mod_lt {m : Nat} (u : UInt8) : m > 0 → (u % UInt8.ofNat m).toNat < m

theorem UInt8.lt_def {a : UInt8} {b : UInt8} : a < b ↔ a.toBitVec < b.toBitVec

theorem UInt8.zero_def : 0 = { toBitVec := 0 }

theorem UInt8.toNat.inj {a : UInt8} {b : UInt8} : a.toNat = b.toNat → a = b

@[simp]

theorem UInt8.toNat_mod (a : UInt8) (b : UInt8) : (a % b).toNat = a.toNat % b.toNat

theorem UInt8.toNat_ofNat_of_lt {n : Nat} (h : n < UInt8.size) : (UInt8.ofNat n).toNat = n

theorem UInt8.eq_of_toBitVec_eq {a : UInt8} {b : UInt8} (h : a.toBitVec = b.toBitVec) : a = b

@[simp]

theorem UInt8.mk_ofNat (n : Nat) : { toBitVec := BitVec.ofNat 8 n } = OfNat.ofNat n

theorem UInt8.lt_asymm {a : UInt8} {b : UInt8} : a < b → ¬b < a

@[simp]

theorem UInt8.mk_toBitVec_eq (a : UInt8) : { toBitVec := a.toBitVec } = a

@[simp]

theorem UInt8.toNat_div (a : UInt8) (b : UInt8) : (a / b).toNat = a.toNat / b.toNat

theorem UInt8.ne_of_toBitVec_ne {a : UInt8} {b : UInt8} (h : a.toBitVec ≠ b.toBitVec) : a ≠ b

@[simp]

theorem UInt8.val_ofNat (n : Nat) : (OfNat.ofNat n).val = OfNat.ofNat n

theorem UInt8.le_def {a : UInt8} {b : UInt8} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec

@[simp]

theorem UInt8.not_lt {a : UInt8} {b : UInt8} : ¬a < b ↔ b ≤ a

theorem UInt8.toBitVec_eq_of_eq {a : UInt8} {b : UInt8} (h : a = b) : a.toBitVec = b.toBitVec

@[simp]

theorem UInt8.toNat_zero : UInt8.toNat 0 = 0

@[simp]

theorem UInt8.le_refl (a : UInt8) : a ≤ a

theorem UInt8.le_trans {a : UInt8} {b : UInt8} {c : UInt8} : a ≤ b → b ≤ c → a ≤ c

@[simp]

theorem UInt8.ofNat_one : UInt8.ofNat 1 = 1

theorem UInt8.mod_lt (a : UInt8) {b : UInt8} : 0 < b → a % b < b

theorem UInt8.mul_def (a : UInt8) (b : UInt8) : a * b = { toBitVec := a.toBitVec * b.toBitVec }

theorem UInt8.one_def : 1 = { toBitVec := 1 }

theorem UInt8.lt_trans {a : UInt8} {b : UInt8} {c : UInt8} : a < b → b < c → a < c

theorem UInt8.mod_def (a : UInt8) (b : UInt8) : a % b = { toBitVec := a.toBitVec % b.toBitVec }

@[simp]

theorem UInt8.toNat_sub_of_le (a : UInt8) (b : UInt8) : b ≤ a → (a - b).toNat = a.toNat - b.toNat

@[deprecated UInt8.toNat_mod_lt]

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

theorem UInt8.le_total (a : UInt8) (b : UInt8) : a ≤ b ∨ b ≤ a

theorem UInt8.eq_of_val_eq {a : UInt8} {b : UInt8} (h : a.val = b.val) : a = b

theorem UInt8.toNat_lt_size (a : UInt8) : a.toNat < UInt8.size

theorem UInt16.lt_asymm {a : UInt16} {b : UInt16} : a < b → ¬b < a

@[simp]

theorem UInt16.toNat_mod (a : UInt16) (b : UInt16) : (a % b).toNat = a.toNat % b.toNat

theorem UInt16.toNat_lt_size (a : UInt16) : a.toNat < UInt16.size

theorem UInt16.le_def {a : UInt16} {b : UInt16} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec

@[simp]

theorem UInt16.toBitVec_ofNat (n : Nat) : (OfNat.ofNat n).toBitVec = BitVec.ofNat 16 n

theorem UInt16.lt_trans {a : UInt16} {b : UInt16} {c : UInt16} : a < b → b < c → a < c

theorem UInt16.toBitVec_eq_of_eq {a : UInt16} {b : UInt16} (h : a = b) : a.toBitVec = b.toBitVec

theorem UInt16.le_total (a : UInt16) (b : UInt16) : a ≤ b ∨ b ≤ a

theorem UInt16.ne_of_lt {a : UInt16} {b : UInt16} (h : a < b) : a ≠ b

@[simp]

theorem UInt16.lt_irrefl (a : UInt16) : ¬a < a

theorem UInt16.one_def : 1 = { toBitVec := 1 }

theorem UInt16.toNat.inj {a : UInt16} {b : UInt16} : a.toNat = b.toNat → a = b

theorem UInt16.zero_def : 0 = { toBitVec := 0 }

theorem UInt16.lt_def {a : UInt16} {b : UInt16} : a < b ↔ a.toBitVec < b.toBitVec

theorem UInt16.mod_def (a : UInt16) (b : UInt16) : a % b = { toBitVec := a.toBitVec % b.toBitVec }

theorem UInt16.sub_def (a : UInt16) (b : UInt16) : a - b = { toBitVec := a.toBitVec - b.toBitVec }

theorem UInt16.mod_lt (a : UInt16) {b : UInt16} : 0 < b → a % b < b

theorem UInt16.toBitVec_eq_of_lt {a : Nat} : a < UInt16.size → (UInt16.ofNat a).toBitVec.toNat = a

theorem UInt16.ne_of_toBitVec_ne {a : UInt16} {b : UInt16} (h : a.toBitVec ≠ b.toBitVec) : a ≠ b

@[simp]

theorem UInt16.mk_toBitVec_eq (a : UInt16) : { toBitVec := a.toBitVec } = a

@[simp]

theorem UInt16.val_ofNat (n : Nat) : (OfNat.ofNat n).val = OfNat.ofNat n

theorem UInt16.mul_def (a : UInt16) (b : UInt16) : a * b = { toBitVec := a.toBitVec * b.toBitVec }

@[simp]

theorem UInt16.mk_ofNat (n : Nat) : { toBitVec := BitVec.ofNat 16 n } = OfNat.ofNat n

theorem UInt16.eq_of_toBitVec_eq {a : UInt16} {b : UInt16} (h : a.toBitVec = b.toBitVec) : a = b

instance UInt16.instInhabited : Inhabited UInt16

Equations

• UInt16.instInhabited = { default := 0 }

@[simp]

theorem UInt16.toNat_sub_of_le (a : UInt16) (b : UInt16) : b ≤ a → (a - b).toNat = a.toNat - b.toNat

theorem UInt16.add_def (a : UInt16) (b : UInt16) : a + b = { toBitVec := a.toBitVec + b.toBitVec }

theorem UInt16.eq_of_val_eq {a : UInt16} {b : UInt16} (h : a.val = b.val) : a = b

@[simp]

theorem UInt16.toNat_div (a : UInt16) (b : UInt16) : (a / b).toNat = a.toNat / b.toNat

@[simp]

theorem UInt16.not_le {a : UInt16} {b : UInt16} : ¬a ≤ b ↔ b < a

theorem UInt16.toNat_mod_lt {m : Nat} (u : UInt16) : m > 0 → (u % UInt16.ofNat m).toNat < m

theorem UInt16.le_trans {a : UInt16} {b : UInt16} {c : UInt16} : a ≤ b → b ≤ c → a ≤ c

@[simp]

theorem UInt16.le_refl (a : UInt16) : a ≤ a

@[deprecated UInt16.toNat_mod_lt]

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

@[simp]

theorem UInt16.not_lt {a : UInt16} {b : UInt16} : ¬a < b ↔ b ≤ a

@[simp]

theorem UInt16.toNat_zero : UInt16.toNat 0 = 0

@[simp]

theorem UInt16.ofNat_one : UInt16.ofNat 1 = 1

theorem UInt16.toNat_ofNat_of_lt {n : Nat} (h : n < UInt16.size) : (UInt16.ofNat n).toNat = n

@[simp]

theorem UInt32.not_lt {a : UInt32} {b : UInt32} : ¬a < b ↔ b ≤ a

theorem UInt32.sub_def (a : UInt32) (b : UInt32) : a - b = { toBitVec := a.toBitVec - b.toBitVec }

theorem UInt32.mul_def (a : UInt32) (b : UInt32) : a * b = { toBitVec := a.toBitVec * b.toBitVec }

theorem UInt32.mod_def (a : UInt32) (b : UInt32) : a % b = { toBitVec := a.toBitVec % b.toBitVec }

theorem UInt32.le_total (a : UInt32) (b : UInt32) : a ≤ b ∨ b ≤ a

@[simp]

theorem UInt32.lt_irrefl (a : UInt32) : ¬a < a

@[simp]

theorem UInt32.mk_ofNat (n : Nat) : { toBitVec := BitVec.ofNat 32 n } = OfNat.ofNat n

theorem UInt32.le_trans {a : UInt32} {b : UInt32} {c : UInt32} : a ≤ b → b ≤ c → a ≤ c

theorem UInt32.eq_of_toBitVec_eq {a : UInt32} {b : UInt32} (h : a.toBitVec = b.toBitVec) : a = b

theorem UInt32.mod_lt (a : UInt32) {b : UInt32} : 0 < b → a % b < b

theorem UInt32.one_def : 1 = { toBitVec := 1 }

theorem UInt32.ne_of_toBitVec_ne {a : UInt32} {b : UInt32} (h : a.toBitVec ≠ b.toBitVec) : a ≠ b

theorem UInt32.le_def {a : UInt32} {b : UInt32} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec

theorem UInt32.add_def (a : UInt32) (b : UInt32) : a + b = { toBitVec := a.toBitVec + b.toBitVec }

theorem UInt32.toNat_ofNat_of_lt {n : Nat} (h : n < UInt32.size) : (UInt32.ofNat n).toNat = n

theorem UInt32.eq_of_val_eq {a : UInt32} {b : UInt32} (h : a.val = b.val) : a = b

@[simp]

theorem UInt32.le_refl (a : UInt32) : a ≤ a

theorem UInt32.toNat.inj {a : UInt32} {b : UInt32} : a.toNat = b.toNat → a = b

@[simp]

theorem UInt32.toNat_sub_of_le (a : UInt32) (b : UInt32) : b ≤ a → (a - b).toNat = a.toNat - b.toNat

@[deprecated UInt32.toNat_mod_lt]

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

theorem UInt32.toNat_mod_lt {m : Nat} (u : UInt32) : m > 0 → (u % UInt32.ofNat m).toNat < m

@[simp]

theorem UInt32.val_ofNat (n : Nat) : (OfNat.ofNat n).val = OfNat.ofNat n

@[simp]

theorem UInt32.ofNat_one : UInt32.ofNat 1 = 1

@[simp]

theorem UInt32.not_le {a : UInt32} {b : UInt32} : ¬a ≤ b ↔ b < a

instance UInt32.instInhabited : Inhabited UInt32

Equations

• UInt32.instInhabited = { default := 0 }

theorem UInt32.ne_of_lt {a : UInt32} {b : UInt32} (h : a < b) : a ≠ b

@[simp]

theorem UInt32.toBitVec_ofNat (n : Nat) : (OfNat.ofNat n).toBitVec = BitVec.ofNat 32 n

theorem UInt32.lt_asymm {a : UInt32} {b : UInt32} : a < b → ¬b < a

theorem UInt32.toBitVec_eq_of_lt {a : Nat} : a < UInt32.size → (UInt32.ofNat a).toBitVec.toNat = a

theorem UInt32.toBitVec_eq_of_eq {a : UInt32} {b : UInt32} (h : a = b) : a.toBitVec = b.toBitVec

@[simp]

theorem UInt32.toNat_zero : UInt32.toNat 0 = 0

@[simp]

theorem UInt32.mk_toBitVec_eq (a : UInt32) : { toBitVec := a.toBitVec } = a

theorem UInt32.lt_def {a : UInt32} {b : UInt32} : a < b ↔ a.toBitVec < b.toBitVec

@[simp]

theorem UInt32.toNat_div (a : UInt32) (b : UInt32) : (a / b).toNat = a.toNat / b.toNat

theorem UInt32.toNat_lt_size (a : UInt32) : a.toNat < UInt32.size

@[simp]

theorem UInt32.toNat_mod (a : UInt32) (b : UInt32) : (a % b).toNat = a.toNat % b.toNat

theorem UInt32.lt_trans {a : UInt32} {b : UInt32} {c : UInt32} : a < b → b < c → a < c

theorem UInt32.zero_def : 0 = { toBitVec := 0 }

instance UInt64.instInhabited : Inhabited UInt64

Equations

• UInt64.instInhabited = { default := 0 }

@[simp]

theorem UInt64.le_refl (a : UInt64) : a ≤ a

theorem UInt64.toNat.inj {a : UInt64} {b : UInt64} : a.toNat = b.toNat → a = b

theorem UInt64.sub_def (a : UInt64) (b : UInt64) : a - b = { toBitVec := a.toBitVec - b.toBitVec }

theorem UInt64.add_def (a : UInt64) (b : UInt64) : a + b = { toBitVec := a.toBitVec + b.toBitVec }

@[simp]

theorem UInt64.lt_irrefl (a : UInt64) : ¬a < a

@[simp]

theorem UInt64.not_le {a : UInt64} {b : UInt64} : ¬a ≤ b ↔ b < a

theorem UInt64.toNat_ofNat_of_lt {n : Nat} (h : n < UInt64.size) : (UInt64.ofNat n).toNat = n

@[simp]

theorem UInt64.toNat_zero : UInt64.toNat 0 = 0

theorem UInt64.le_def {a : UInt64} {b : UInt64} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec

theorem UInt64.eq_of_val_eq {a : UInt64} {b : UInt64} (h : a.val = b.val) : a = b

theorem UInt64.lt_def {a : UInt64} {b : UInt64} : a < b ↔ a.toBitVec < b.toBitVec

theorem UInt64.eq_of_toBitVec_eq {a : UInt64} {b : UInt64} (h : a.toBitVec = b.toBitVec) : a = b

@[simp]

theorem UInt64.toBitVec_ofNat (n : Nat) : (OfNat.ofNat n).toBitVec = BitVec.ofNat 64 n

@[simp]

theorem UInt64.mk_ofNat (n : Nat) : { toBitVec := BitVec.ofNat 64 n } = OfNat.ofNat n

theorem UInt64.ne_of_lt {a : UInt64} {b : UInt64} (h : a < b) : a ≠ b

@[simp]

theorem UInt64.not_lt {a : UInt64} {b : UInt64} : ¬a < b ↔ b ≤ a

theorem UInt64.toBitVec_eq_of_lt {a : Nat} : a < UInt64.size → (UInt64.ofNat a).toBitVec.toNat = a

@[simp]

theorem UInt64.toNat_mod (a : UInt64) (b : UInt64) : (a % b).toNat = a.toNat % b.toNat

theorem UInt64.mod_lt (a : UInt64) {b : UInt64} : 0 < b → a % b < b

@[simp]

theorem UInt64.toNat_div (a : UInt64) (b : UInt64) : (a / b).toNat = a.toNat / b.toNat

theorem UInt64.toNat_lt_size (a : UInt64) : a.toNat < UInt64.size

@[simp]

theorem UInt64.mk_toBitVec_eq (a : UInt64) : { toBitVec := a.toBitVec } = a

theorem UInt64.lt_asymm {a : UInt64} {b : UInt64} : a < b → ¬b < a

theorem UInt64.mod_def (a : UInt64) (b : UInt64) : a % b = { toBitVec := a.toBitVec % b.toBitVec }

theorem UInt64.le_total (a : UInt64) (b : UInt64) : a ≤ b ∨ b ≤ a

theorem UInt64.toNat_mod_lt {m : Nat} (u : UInt64) : m > 0 → (u % UInt64.ofNat m).toNat < m

@[simp]

theorem UInt64.ofNat_one : UInt64.ofNat 1 = 1

theorem UInt64.lt_trans {a : UInt64} {b : UInt64} {c : UInt64} : a < b → b < c → a < c

theorem UInt64.le_trans {a : UInt64} {b : UInt64} {c : UInt64} : a ≤ b → b ≤ c → a ≤ c

@[deprecated UInt64.toNat_mod_lt]

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

@[simp]

theorem UInt64.val_ofNat (n : Nat) : (OfNat.ofNat n).val = OfNat.ofNat n

theorem UInt64.mul_def (a : UInt64) (b : UInt64) : a * b = { toBitVec := a.toBitVec * b.toBitVec }

theorem UInt64.zero_def : 0 = { toBitVec := 0 }

theorem UInt64.one_def : 1 = { toBitVec := 1 }

theorem UInt64.ne_of_toBitVec_ne {a : UInt64} {b : UInt64} (h : a.toBitVec ≠ b.toBitVec) : a ≠ b

@[simp]

theorem UInt64.toNat_sub_of_le (a : UInt64) (b : UInt64) : b ≤ a → (a - b).toNat = a.toNat - b.toNat

theorem UInt64.toBitVec_eq_of_eq {a : UInt64} {b : UInt64} (h : a = b) : a.toBitVec = b.toBitVec

instance USize.instInhabited : Inhabited USize

Equations

• USize.instInhabited = { default := 0 }

theorem USize.toBitVec_eq_of_eq {a : USize} {b : USize} (h : a = b) : a.toBitVec = b.toBitVec

theorem USize.mod_lt (a : USize) {b : USize} : 0 < b → a % b < b

theorem USize.one_def : 1 = { toBitVec := 1 }

theorem USize.mul_def (a : USize) (b : USize) : a * b = { toBitVec := a.toBitVec * b.toBitVec }

@[simp]

theorem USize.toNat_mod (a : USize) (b : USize) : (a % b).toNat = a.toNat % b.toNat

theorem USize.toBitVec_eq_of_lt {a : Nat} : a < USize.size → (USize.ofNat a).toBitVec.toNat = a

@[simp]

theorem USize.le_refl (a : USize) : a ≤ a

theorem USize.le_def {a : USize} {b : USize} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec

theorem USize.toNat_ofNat_of_lt {n : Nat} (h : n < USize.size) : (USize.ofNat n).toNat = n

@[simp]

theorem USize.mk_ofNat (n : Nat) : { toBitVec := BitVec.ofNat System.Platform.numBits n } = OfNat.ofNat n

@[simp]

theorem USize.toNat_div (a : USize) (b : USize) : (a / b).toNat = a.toNat / b.toNat

theorem USize.le_total (a : USize) (b : USize) : a ≤ b ∨ b ≤ a

@[simp]

theorem USize.mk_toBitVec_eq (a : USize) : { toBitVec := a.toBitVec } = a

theorem USize.sub_def (a : USize) (b : USize) : a - b = { toBitVec := a.toBitVec - b.toBitVec }

@[simp]

theorem USize.lt_irrefl (a : USize) : ¬a < a

@[simp]

theorem USize.not_le {a : USize} {b : USize} : ¬a ≤ b ↔ b < a

theorem USize.eq_of_val_eq {a : USize} {b : USize} (h : a.val = b.val) : a = b

theorem USize.toNat_lt_size (a : USize) : a.toNat < USize.size

theorem USize.add_def (a : USize) (b : USize) : a + b = { toBitVec := a.toBitVec + b.toBitVec }

theorem USize.eq_of_toBitVec_eq {a : USize} {b : USize} (h : a.toBitVec = b.toBitVec) : a = b

@[simp]

theorem USize.ofNat_one : USize.ofNat 1 = 1

@[simp]

theorem USize.not_lt {a : USize} {b : USize} : ¬a < b ↔ b ≤ a

@[simp]

theorem USize.toBitVec_ofNat (n : Nat) : (OfNat.ofNat n).toBitVec = BitVec.ofNat System.Platform.numBits n

theorem USize.lt_asymm {a : USize} {b : USize} : a < b → ¬b < a

theorem USize.le_trans {a : USize} {b : USize} {c : USize} : a ≤ b → b ≤ c → a ≤ c

theorem USize.ne_of_toBitVec_ne {a : USize} {b : USize} (h : a.toBitVec ≠ b.toBitVec) : a ≠ b

@[deprecated USize.toNat_mod_lt]

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

theorem USize.zero_def : 0 = { toBitVec := 0 }

@[simp]

theorem USize.toNat_zero : USize.toNat 0 = 0

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

theorem USize.lt_trans {a : USize} {b : USize} {c : USize} : a < b → b < c → a < c

theorem USize.ne_of_lt {a : USize} {b : USize} (h : a < b) : a ≠ b

@[simp]

theorem USize.val_ofNat (n : Nat) : (OfNat.ofNat n).val = OfNat.ofNat n

theorem USize.mod_def (a : USize) (b : USize) : a % b = { toBitVec := a.toBitVec % b.toBitVec }

@[simp]

theorem USize.toNat_sub_of_le (a : USize) (b : USize) : b ≤ a → (a - b).toNat = a.toNat - b.toNat

theorem USize.toNat.inj {a : USize} {b : USize} : a.toNat = b.toNat → a = b

theorem USize.lt_def {a : USize} {b : USize} : a < b ↔ a.toBitVec < b.toBitVec

theorem UInt32.toNat_lt_of_lt {n : UInt32} {m : Nat} (h : m < UInt32.size) : n < UInt32.ofNat m → n.toNat < m

theorem UInt32.lt_toNat_of_lt {n : UInt32} {m : Nat} (h : m < UInt32.size) : UInt32.ofNat m < n → m < n.toNat

theorem UInt32.toNat_le_of_le {n : UInt32} {m : Nat} (h : m < UInt32.size) : n ≤ UInt32.ofNat m → n.toNat ≤ m

theorem UInt32.le_toNat_of_le {n : UInt32} {m : Nat} (h : m < UInt32.size) : UInt32.ofNat m ≤ n → m ≤ n.toNat

@[reducible, inline, deprecated]

abbrev UInt8.zero_toNat : UInt8.toNat 0 = 0

Equations

• UInt8.zero_toNat = UInt8.toNat_zero

@[reducible, inline, deprecated]

abbrev UInt8.div_toNat (a : UInt8) (b : UInt8) : (a / b).toNat = a.toNat / b.toNat

Equations

• UInt8.div_toNat = UInt8.toNat_div

@[reducible, inline, deprecated]

abbrev UInt8.mod_toNat (a : UInt8) (b : UInt8) : (a % b).toNat = a.toNat % b.toNat

Equations

• UInt8.mod_toNat = UInt8.toNat_mod

@[reducible, inline, deprecated]

abbrev UInt16.zero_toNat : UInt16.toNat 0 = 0

Equations

• UInt16.zero_toNat = UInt16.toNat_zero

@[reducible, inline, deprecated]

abbrev UInt16.div_toNat (a : UInt16) (b : UInt16) : (a / b).toNat = a.toNat / b.toNat

Equations

• UInt16.div_toNat = UInt16.toNat_div

@[reducible, inline, deprecated]

abbrev UInt16.mod_toNat (a : UInt16) (b : UInt16) : (a % b).toNat = a.toNat % b.toNat

Equations

• UInt16.mod_toNat = UInt16.toNat_mod

@[reducible, inline, deprecated]

abbrev UInt32.zero_toNat : UInt32.toNat 0 = 0

Equations

• UInt32.zero_toNat = UInt32.toNat_zero

@[reducible, inline, deprecated]

abbrev UInt32.div_toNat (a : UInt32) (b : UInt32) : (a / b).toNat = a.toNat / b.toNat

Equations

• UInt32.div_toNat = UInt32.toNat_div

@[reducible, inline, deprecated]

abbrev UInt32.mod_toNat (a : UInt32) (b : UInt32) : (a % b).toNat = a.toNat % b.toNat

Equations

• UInt32.mod_toNat = UInt32.toNat_mod

@[reducible, inline, deprecated]

abbrev UInt64.zero_toNat : UInt64.toNat 0 = 0

Equations

• UInt64.zero_toNat = UInt64.toNat_zero

@[reducible, inline, deprecated]

abbrev UInt64.div_toNat (a : UInt64) (b : UInt64) : (a / b).toNat = a.toNat / b.toNat

Equations

• UInt64.div_toNat = UInt64.toNat_div

@[reducible, inline, deprecated]

abbrev UInt64.mod_toNat (a : UInt64) (b : UInt64) : (a % b).toNat = a.toNat % b.toNat

Equations

• UInt64.mod_toNat = UInt64.toNat_mod

@[reducible, inline, deprecated]

abbrev USize.zero_toNat : USize.toNat 0 = 0

Equations

• USize.zero_toNat = USize.toNat_zero

@[reducible, inline, deprecated]

abbrev USize.div_toNat (a : USize) (b : USize) : (a / b).toNat = a.toNat / b.toNat

Equations

• USize.div_toNat = USize.toNat_div

@[reducible, inline, deprecated]

abbrev USize.mod_toNat (a : USize) (b : USize) : (a % b).toNat = a.toNat % b.toNat

Equations

• USize.mod_toNat = USize.toNat_mod