mathlib documentation

data.string.basic

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

Equations

string.ltb s₁ s₂ = s₂.has_next.cases_on ff ((λ (_x : bool) (h₁ : s₁.has_next = _x), _x.cases_on (λ (h₁ : s₁.has_next = ff), tt) (λ (h₁ : s₁.has_next = tt), ite (s₁.curr = s₂.curr) (string.ltb s₁.next s₂.next) (to_bool (s₁.curr < s₂.curr))) h₁) s₁.has_next _)

@[instance]

def string.has_lt' :

Equations

string.has_lt' = {lt := λ (s₁ s₂ : string), ↥(string.ltb s₁.mk_iterator s₂.mk_iterator)}

@[instance]

def string.decidable_lt :

decidable_rel has_lt.lt

Equations

string.decidable_lt = λ (a b : string), bool.decidable_eq (string.ltb a.mk_iterator b.mk_iterator) tt

@[simp]

theorem string.lt_iff_to_list_lt {s₁ s₂ : string} :

s₁ < s₂ ↔ s₁.to_list < s₂.to_list

@[instance]

def string.has_le :

Equations

string.has_le = {le := λ (s₁ s₂ : string), ¬s₂ < s₁}

@[instance]

def string.decidable_le :

decidable_rel has_le.le

Equations

string.decidable_le = λ (a b : string), ne.decidable (string.ltb b.mk_iterator a.mk_iterator) tt

@[simp]

theorem string.le_iff_to_list_le {s₁ s₂ : string} :

s₁ ≤ s₂ ↔ s₁.to_list ≤ s₂.to_list

theorem string.to_list_inj {s₁ s₂ : string} :

s₁.to_list = s₂.to_list ↔ s₁ = s₂

@[instance]

def string.decidable_linear_order :

decidable_linear_order string

Equations

string.decidable_linear_order = {le := has_le.le string.has_le, lt := has_lt.lt string.has_lt', le_refl := string.decidable_linear_order._proof_1, le_trans := string.decidable_linear_order._proof_2, lt_iff_le_not_le := string.decidable_linear_order._proof_3, le_antisymm := string.decidable_linear_order._proof_4, le_total := string.decidable_linear_order._proof_5, decidable_le := string.decidable_le, decidable_eq := λ (a b : string), string.has_decidable_eq a b, decidable_lt := λ (a b : string), string.decidable_lt a b}