mathlib3 documentation

core / init.data.string.basic

structure string_imp  :

In the VM, strings are implemented using a dynamic array and UTF-8 encoding.

TODO: we currently cannot mark string_imp as private because we need to bind string_imp.mk and string_imp.cases_on in the VM.

Instances for string_imp
Equations
@[protected, instance]
Equations
@[protected, instance]
def string.has_decidable_lt (s₁ s₂ : string) :
decidable (s₁ < s₂)

Remark: this function has a VM builtin efficient implementation.

Equations
@[protected, instance]
Equations
Equations

The internal implementation uses dynamic arrays and will perform destructive updates if the string is not shared.

Equations

The internal implementation uses dynamic arrays and will perform destructive updates if the string is not shared.

Equations

O(n) in the VM, where n is the length of the string

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

In the VM, the string iterator is implemented as a pointer to the string being iterated + index.

TODO: we currently cannot mark interator_imp as private because we need to bind string_imp.mk and string_imp.cases_on in the VM.

Instances for string.iterator_imp

In the VM, set_curr is constant time if the string being iterated is not shared and linear time if it is.

Equations

In the VM, to_string is a constant time operation.

Equations
@[protected]
Equations
Equations

The following definitions do not have builtin support in the VM

@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
def string.front (s : string) :
Equations
def string.back (s : string) :
Equations
def string.join (l : list string) :
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₂