mathlib documentation

data.string.basic

Strings #

Supplementary theorems about the string type.

< on string iterators. This coincides with < on strings as lists.

Equations
@[protected, instance]
Equations
@[simp]
theorem string.lt_iff_to_list_lt {s₁ s₂ : string} :
s₁ < s₂ s₁.to_list < s₂.to_list
@[protected, 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} :
s ""s.to_list = s.head :: (s.popn 1).to_list
@[simp]
theorem string.head_empty  :
@[simp]
theorem string.popn_empty {n : } :
"".popn n = ""
@[protected, instance]
Equations
@[simp]
@[simp]
theorem list.as_string_inj {l l' : list char} :
@[simp]
theorem list.as_string_eq {l : list char} {s : string} :