@[instance_reducible]

instance String.instLT : LT String

Equations

• String.instLT = { lt := fun (s₁ s₂ : String) => s₁.toByteArray < s₂.toByteArray }

@[instance_reducible, extern lean_string_dec_lt]

instance String.decidableLT (s₁ s₂ : String) : Decidable (s₁ < s₂)

Equations

• s₁.decidableLT s₂ = s₁.toByteArray.instDecidableLT s₂.toByteArray

@[reducible]

def String.le (a b : String) : Prop

Non-strict inequality on strings, typically used via the ≤ operator.

a ≤ b is defined to mean ¬ b < a.

Equations

• a.le b = ¬b < a

@[instance_reducible]

instance String.instLE : LE String

Equations

• String.instLE = { le := String.le }

@[instance_reducible]

instance String.decLE (s₁ s₂ : String) : Decidable (s₁ ≤ s₂)

Equations

• s₁.decLE s₂ = { decide := !decide (s₂ < s₁), reflects_decide := ⋯ }

@[simp]

theorem String.toByteArray_lt_toByteArray_iff {s t : String} : s.toByteArray < t.toByteArray ↔ s < t

@[simp]

theorem String.toByteArray_le_toByteArray_iff {s t : String} : s.toByteArray ≤ t.toByteArray ↔ s ≤ t

instance String.instLawfulOrderLT : Std.LawfulOrderLT String

@[extern lean_string_compare]

def String.compare (s₁ s₂ : String) : Ordering

Lexicographic comparison of strings

Equations

• s₁.compare s₂ = compare s₁.toByteArray s₂.toByteArray

@[instance_reducible]

instance String.instOrd : Ord String

Equations

• String.instOrd = { compare := String.compare }

@[simp]

theorem String.compare_toByteArray_toByteArray {s t : String} : compare s.toByteArray t.toByteArray = compare s t

instance String.instLawfulOrderOrd : Std.LawfulOrderOrd String

instance String.instTransOrd : Std.TransOrd String

instance String.instLawfulEqOrd : Std.LawfulEqOrd String

instance String.instIsLinearOrder : Std.IsLinearOrder String

@[instance_reducible]

instance String.instLinearOrderPackage : Std.LinearOrderPackage String

Equations

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