def commandDeclare_uint_theorems_ : Lean.ParserDescr

Equations

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

@[simp]

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

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

@[simp]

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

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

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

@[simp]

theorem UInt8.mk_val_eq (a : UInt8) : { val := a.val } = a

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

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

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

theorem UInt8.ne_of_val_ne {a : UInt8} {b : UInt8} (h : a.val ≠ b.val) : a ≠ b

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

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

@[simp]

theorem UInt8.ofNat_one : UInt8.ofNat 1 = 1

@[simp]

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

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

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

@[simp]

theorem UInt8.modn_toNat (a : UInt8) (b : Nat) : (a.modn b).toNat = a.toNat % b

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

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

instance UInt8.instInhabited : Inhabited UInt8

Equations

• UInt8.instInhabited = { default := 0 }

@[simp]

theorem UInt8.zero_toNat : UInt8.toNat 0 = 0

theorem UInt8.mod_lt (a : UInt8) (b : UInt8) (h : 0 < b) : a % b < b

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem UInt8.val_eq_of_lt {a : Nat} : a < UInt8.size → ↑(UInt8.ofNat a).val = a

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

theorem UInt8.lt_iff_val_lt_val {a : UInt8} {b : UInt8} : a < b ↔ a.val < b.val

theorem UInt8.lt_asymm {a : UInt8} {b : UInt8} (h : a < b) : ¬b < a

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

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

@[simp]

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

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

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

theorem UInt16.lt_asymm {a : UInt16} {b : UInt16} (h : a < b) : ¬b < a

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

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

@[simp]

theorem UInt16.zero_toNat : UInt16.toNat 0 = 0

@[simp]

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

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

@[simp]

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

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

@[simp]

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

theorem UInt16.ne_of_val_ne {a : UInt16} {b : UInt16} (h : a.val ≠ b.val) : a ≠ b

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

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

@[simp]

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

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

@[simp]

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

@[simp]

theorem UInt16.modn_toNat (a : UInt16) (b : Nat) : (a.modn b).toNat = a.toNat % b

@[simp]

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

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

@[simp]

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

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

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

theorem UInt16.lt_iff_val_lt_val {a : UInt16} {b : UInt16} : a < b ↔ a.val < b.val

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

theorem UInt16.mod_lt (a : UInt16) (b : UInt16) (h : 0 < b) : a % b < b

@[simp]

theorem UInt16.mk_val_eq (a : UInt16) : { val := a.val } = a

instance UInt16.instInhabited : Inhabited UInt16

Equations

• UInt16.instInhabited = { default := 0 }

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

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

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

theorem UInt16.val_eq_of_lt {a : Nat} : a < UInt16.size → ↑(UInt16.ofNat a).val = a

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

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

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

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

@[simp]

theorem UInt16.ofNat_one : UInt16.ofNat 1 = 1

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

@[simp]

theorem UInt32.zero_toNat : UInt32.toNat 0 = 0

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

instance UInt32.instInhabited : Inhabited UInt32

Equations

• UInt32.instInhabited = { default := 0 }

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

theorem UInt32.ne_of_val_ne {a : UInt32} {b : UInt32} (h : a.val ≠ b.val) : a ≠ b

@[simp]

theorem UInt32.mk_val_eq (a : UInt32) : { val := a.val } = a

@[simp]

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

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

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

theorem UInt32.val_eq_of_lt {a : Nat} : a < UInt32.size → ↑(UInt32.ofNat a).val = a

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

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

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

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

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

@[simp]

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

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

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

@[simp]

theorem UInt32.ofNat_one : UInt32.ofNat 1 = 1

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

@[simp]

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

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

@[simp]

theorem UInt32.modn_toNat (a : UInt32) (b : Nat) : (a.modn b).toNat = a.toNat % b

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

theorem UInt32.lt_iff_val_lt_val {a : UInt32} {b : UInt32} : a < b ↔ a.val < b.val

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem UInt32.mod_lt (a : UInt32) (b : UInt32) (h : 0 < b) : a % b < b

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

theorem UInt32.lt_asymm {a : UInt32} {b : UInt32} (h : a < b) : ¬b < a

@[simp]

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

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

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

@[simp]

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

@[simp]

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

theorem UInt64.lt_asymm {a : UInt64} {b : UInt64} (h : a < b) : ¬b < a

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

@[simp]

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

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

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

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

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

@[simp]

theorem UInt64.ofNat_one : UInt64.ofNat 1 = 1

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

@[simp]

theorem UInt64.modn_toNat (a : UInt64) (b : Nat) : (a.modn b).toNat = a.toNat % b

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

@[simp]

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

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

@[simp]

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

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

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

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

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

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

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.one_def : 1 = { val := 1 }

theorem UInt64.mod_lt (a : UInt64) (b : UInt64) (h : 0 < b) : a % b < b

instance UInt64.instInhabited : Inhabited UInt64

Equations

• UInt64.instInhabited = { default := 0 }

@[simp]

theorem UInt64.mk_val_eq (a : UInt64) : { val := a.val } = a

@[simp]

theorem UInt64.zero_toNat : UInt64.toNat 0 = 0

theorem UInt64.ne_of_val_ne {a : UInt64} {b : UInt64} (h : a.val ≠ b.val) : a ≠ b

theorem UInt64.val_eq_of_lt {a : Nat} : a < UInt64.size → ↑(UInt64.ofNat a).val = a

theorem UInt64.lt_iff_val_lt_val {a : UInt64} {b : UInt64} : a < b ↔ a.val < b.val

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

@[simp]

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

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

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

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

theorem USize.mod_lt (a : USize) (b : USize) (h : 0 < b) : a % b < b

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

@[simp]

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

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

@[simp]

theorem USize.zero_toNat : USize.toNat 0 = 0

@[simp]

theorem USize.modn_toNat (a : USize) (b : Nat) : (a.modn b).toNat = a.toNat % b

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

theorem USize.val_eq_of_lt {a : Nat} : a < USize.size → ↑(USize.ofNat a).val = a

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

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

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

@[simp]

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

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

theorem USize.ne_of_val_ne {a : USize} {b : USize} (h : a.val ≠ b.val) : a ≠ b

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

@[simp]

theorem USize.mk_val_eq (a : USize) : { val := a.val } = a

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

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

@[simp]

theorem USize.ofNat_one : USize.ofNat 1 = 1

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

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

instance USize.instInhabited : Inhabited USize

Equations

• USize.instInhabited = { default := 0 }

@[simp]

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

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

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

@[simp]

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

theorem USize.lt_asymm {a : USize} {b : USize} (h : a < b) : ¬b < a

theorem USize.lt_iff_val_lt_val {a : USize} {b : USize} : a < b ↔ a.val < b.val