mathlib documentation

data.string.basic

Equations
@[instance]

Equations
@[simp]
theorem string.lt_iff_to_list_lt {s₁ s₂ : string} :
s₁ < s₂ s₁.to_list < s₂.to_list

@[instance]

Equations
@[simp]
theorem string.le_iff_to_list_le {s₁ s₂ : string} :
s₁ s₂ s₁.to_list s₂.to_list

theorem string.to_list_inj {s₁ s₂ : string} :
s₁.to_list = s₂.to_list s₁ = s₂

@[instance]

Equations