mathlib documentation

core / init.data.string.basic

structure string_imp  :
Type
def string  :
Type
Equations
Equations
@[protected, instance]
Equations
@[protected, instance]
def string.has_decidable_lt (s₁ s₂ : string) :
decidable (s₁ < s₂)
Equations
@[protected, instance]
Equations
Equations
def string.length  :
Equations
def string.push  :
Equations
def string.append  :
Equations
Equations
def string.fold {α : Type u_1} (a : α) (f : α → char → α) (s : string) :
α
Equations
structure string.iterator_imp  :
Type
Equations
@[protected]
Equations
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
def string.is_empty (s : string) :
Equations
def string.front (s : string) :
Equations
def string.back (s : string) :
Equations
def string.join (l : list string) :
Equations
Equations
Equations
Equations
def string.backn (s : string) (n : ) :
Equations
@[protected]
def char.to_string (c : char) :
Equations
def string.to_nat (s : string) :
Equations
theorem string.empty_ne_str (c : char) (s : string) :
"" s.str c
theorem string.str_ne_empty (c : char) (s : string) :
s.str c ""
theorem string.str_ne_str_left {c₁ c₂ : char} (s₁ s₂ : string) :
c₁ c₂s₁.str c₁ s₂.str c₂
theorem string.str_ne_str_right (c₁ c₂ : char) {s₁ s₂ : string} :
s₁ s₂s₁.str c₁ s₂.str c₂