Documentation

Init.Data.String.Compare

@[instance_reducible]

instance String.instLT :

@[instance_reducible, extern lean_string_dec_lt]

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

Decidable (s₁ < s₂)

@[reducible]

def String.le (a b : String) :

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

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

Instances For

@[instance_reducible]

instance String.instLE :

@[instance_reducible]

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

Decidable (s₁ ≤ s₂)

@[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) :

Lexicographic comparison of strings

Instances For

@[instance_reducible]

instance String.instOrd :

@[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