mathlib documentation

def string  :

def list.as_string (s : list char) :

def string.has_lt  :

def string.has_decidable_lt (s₁ s₂ : string) :

def string.has_decidable_eq  :

def string.empty  :

def string.length (a : string) :

def string.push (a : string) (a_1 : char) :

def string.append (a a_1 : string) :

def string.to_list (a : string) :

def string.fold {α : Type u_1} (a : α) (f : α → char → α) (s : string) :

def string.iterator  :

def string.mk_iterator (a : string) :

def string.iterator.curr (a : string.iterator) :

def string.iterator.set_curr (a : string.iterator) (a_1 : char) :

def string.iterator.next (a : string.iterator) :

def string.iterator.prev (a : string.iterator) :

def string.iterator.has_next (a : string.iterator) :

def string.iterator.has_prev (a : string.iterator) :

def string.iterator.insert (a : string.iterator) (a_1 : string) :

def string.iterator.remove (a : string.iterator) (a_1 : ℕ) :

def string.iterator.to_string (a : string.iterator) :

def string.iterator.to_end (a : string.iterator) :

def string.iterator.next_to_string (a : string.iterator) :

def string.iterator.prev_to_string (a : string.iterator) :

def string.iterator.extract_core (a a_1 : list char) :

def string.iterator.extract (a a_1 : string.iterator) :

def string.inhabited  :

def string.has_sizeof  :

def string.has_append  :

def string.str (a : string) (a_1 : char) :

def string.is_empty (s : string) :

def string.front (s : string) :

def string.back (s : string) :

def string.join (l : list string) :

def string.singleton (c : char) :

def string.intercalate (s : string) (ss : list string) :

def string.iterator.nextn (a : string.iterator) (a_1 : ℕ) :

def string.iterator.prevn (a : string.iterator) (a_1 : ℕ) :

def string.pop_back (s : string) :

def string.popn_back (s : string) (n : ℕ) :

def string.backn (s : string) (n : ℕ) :

def char.to_string (c : char) :

def string.to_nat (s : string) :