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₂

@[simp]

@[simp]

theorem string.to_list_nonempty {s : string} (h : s "") :

@[simp]

@[simp]
theorem string.popn_empty {n : } :
"".popn n = ""

@[instance]

Equations
@[simp]
theorem list.as_string_inj {l l' : list char} :

theorem list.as_string_eq {l : list char} {s : string} :