mathlib documentation

core.init.data.string.basic

structure string_imp  :
Type

def string  :
Type

Equations

Equations
@[instance]

Equations
@[instance]
def string.has_decidable_lt (s₁ s₂ : string) :
decidable (s₁ < s₂)

Equations
@[instance]

Equations

Equations
def string.length  :

Equations
def string.push  :

Equations
def string.append  :

Equations

Equations
def string.fold {α : Type u_1} :
α → (α → char → α)string → α

Equations
structure string.iterator_imp  :
Type

Equations

Equations

Equations
@[instance]

Equations

Equations
def string.front  :

Equations

Equations

Equations

Equations

Equations
def string.to_nat  :

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₂