Instances for strings.

@[extern lean_string_compare]

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

Lexicographic comparison of strings

Equations

• s₁.compare s₂ = compareOfLessAndEq s₁ s₂

@[implicit_reducible]

instance String.instOrd : Ord String

Equations

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

instance String.instTransOrd : Std.TransOrd String

instance String.instLawfulEqOrd : Std.LawfulEqOrd String

instance Char.instTransOrd : Std.TransOrd Char

instance Char.instLawfulEqOrd : Std.LawfulEqOrd Char