mathlib3 documentation

core / init.data.string.ops

@[simp]

theorem string.iterator.next_to_string_mk_iterator (s : string) :

s.mk_iterator.next_to_string = s

@[simp]

theorem string.iterator.length_next_to_string_next (it : string.iterator) :

it.next.next_to_string.length = it.next_to_string.length - 1

theorem string.iterator.zero_lt_length_next_to_string_of_has_next {it : string.iterator} :

↥(it.has_next) → 0 < it.next_to_string.length

def string.split (p : char → bool) (s : string) :

Equations

string.split p s = split_core p s.mk_iterator s.mk_iterator