core / init.data.string.basic

string.has_decidable_eq = λ (_x : string), string.has_decidable_eq._match_3 _x
string.has_decidable_eq._match_3 {data := x} = λ (_x : string), string.has_decidable_eq._match_2 x _x
string.has_decidable_eq._match_2 x {data := y} = string.has_decidable_eq._match_1 x y (list.has_dec_eq x y)
string.has_decidable_eq._match_1 x y (is_true p) = is_true _
string.has_decidable_eq._match_1 x y (is_false p) = is_false _

source

def string.empty :

string

Equations

"" = {data := list.nil char}

source

def string.length :

string → ℕ

Equations

string.length {data := s} = s.length

source

def string.push :

string → char → string

Equations

string.push {data := s} c = {data := s ++ [c]}

source

def string.append :

string → string → string

Equations

string.append {data := a} {data := b} = {data := a ++ b}

source

def string.to_list :

string → list char

Equations

string.to_list {data := s} = s

source

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

α

Equations

string.fold a f s = list.foldl f a s.to_list

source

structure string.iterator_imp :

Type

fst : list char
snd : list char

source

def string.iterator :

Type

Equations

string.iterator = string.iterator_imp

source

def string.mk_iterator :

string → string.iterator

Equations

string.mk_iterator {data := s} = {fst := list.nil char, snd := s}

source

def string.iterator.curr :

string.iterator → char

Equations

string.iterator.curr {fst := p, snd := c :: n} = c
string.iterator.curr {fst := fst, snd := list.nil char} = default

source

def string.iterator.set_curr :

string.iterator → char → string.iterator

Equations

string.iterator.set_curr {fst := p, snd := c :: n} c' = {fst := p, snd := c' :: n}
string.iterator.set_curr {fst := fst, snd := list.nil char} c' = {fst := fst, snd := list.nil char}

source

def string.iterator.next :

string.iterator → string.iterator

Equations

string.iterator.next {fst := p, snd := c :: n} = {fst := c :: p, snd := n}
string.iterator.next {fst := p, snd := list.nil char} = {fst := p, snd := list.nil char}

source

def string.iterator.prev :

string.iterator → string.iterator

Equations

string.iterator.prev {fst := c :: p, snd := n} = {fst := p, snd := c :: n}
string.iterator.prev {fst := list.nil char, snd := n} = {fst := list.nil char, snd := n}

source

def string.iterator.has_next :

string.iterator → bool

Equations

string.iterator.has_next {fst := fst, snd := hd :: tl} = tt
string.iterator.has_next {fst := p, snd := list.nil char} = ff

source

def string.iterator.has_prev :

string.iterator → bool

Equations

string.iterator.has_prev {fst := hd :: tl, snd := snd} = tt
string.iterator.has_prev {fst := list.nil char, snd := n} = ff

source

def string.iterator.insert :

string.iterator → string → string.iterator

Equations

string.iterator.insert {fst := p, snd := n} {data := s} = {fst := p, snd := s ++ n}

source

def string.iterator.remove :

string.iterator → ℕ → string.iterator

Equations

string.iterator.remove {fst := p, snd := n} m = {fst := p, snd := list.drop m n}

source

def string.iterator.to_string :

string.iterator → string

Equations

string.iterator.to_string {fst := p, snd := n} = {data := p.reverse ++ n}

source

def string.iterator.to_end :

string.iterator → string.iterator

Equations

string.iterator.to_end {fst := p, snd := n} = {fst := n.reverse ++ p, snd := list.nil char}

source

def string.iterator.next_to_string :

string.iterator → string

Equations

string.iterator.next_to_string {fst := p, snd := n} = {data := n}

source

def string.iterator.prev_to_string :

string.iterator → string

Equations

string.iterator.prev_to_string {fst := p, snd := n} = {data := p.reverse}

source

@[protected]

def string.iterator.extract_core :

list char → list char → option (list char)

Equations

string.iterator.extract_core (c :: cs₁) cs₂ = ite (cs₁ = cs₂) (some [c]) (string.iterator.extract_core._match_1 c (string.iterator.extract_core cs₁ cs₂))
string.iterator.extract_core list.nil cs = none
string.iterator.extract_core._match_1 c (some r) = some (c :: r)
string.iterator.extract_core._match_1 c none = none

source

def string.iterator.extract :

string.iterator → string.iterator → option string

Equations

string.iterator.extract {fst := p₁, snd := n₁} {fst := p₂, snd := n₂} = ite (p₁.reverse ++ n₁ ≠ p₂.reverse ++ n₂) none (ite (n₁ = n₂) (some "") (string.iterator.extract._match_1 (string.iterator.extract_core n₁ n₂)))
string.iterator.extract._match_1 (some r) = some {data := r}
string.iterator.extract._match_1 none = none