theorem String.data_eq_of_eq {a b : String} (h : a = b) : a.data = b.data

theorem String.ne_of_data_ne {a b : String} (h : a.data ≠ b.data) : a ≠ b

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

theorem String.le_antisymm {a b : String} : a ≤ b → b ≤ a → a = b

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

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

instance String.ltIrrefl : Std.Irrefl fun (x1 x2 : Char) => x1 < x2

instance String.leRefl : Std.Refl fun (x1 x2 : Char) => x1 ≤ x2

instance String.leTrans : Trans (fun (x1 x2 : Char) => x1 ≤ x2) (fun (x1 x2 : Char) => x1 ≤ x2) fun (x1 x2 : Char) => x1 ≤ x2

Equations

• String.leTrans = { trans := ⋯ }

instance String.leAntisymm : Std.Antisymm fun (x1 x2 : Char) => x1 ≤ x2

instance String.ltAsymm : Std.Asymm fun (x1 x2 : Char) => x1 < x2

instance String.leTotal : Std.Total fun (x1 x2 : Char) => x1 ≤ x2