Strings

Supplementary theorems about the String type.

@[irreducible]

def String.ltb (s₁ s₂ : Legacy.Iterator) : Bool

< on string iterators. This coincides with < on strings as lists.

Equations

• String.ltb s₁ s₂ = if s₂.hasNext = true then if s₁.hasNext = true then if s₁.curr = s₂.curr then String.ltb s₁.next s₂.next else decide (s₁.curr < s₂.curr) else true else false

@[irreducible]

def String.ltb.inductionOn {motive : Legacy.Iterator → Legacy.Iterator → Sort u} (it₁ it₂ : Legacy.Iterator) (ind : (s₁ s₂ : String) → (i₁ i₂ : Pos.Raw) → { s := s₂, i := i₂ }.hasNext = true → { s := s₁, i := i₁ }.hasNext = true → Pos.Raw.get s₁ i₁ = Pos.Raw.get s₂ i₂ → motive { s := s₁, i := i₁ }.next { s := s₂, i := i₂ }.next → motive { s := s₁, i := i₁ } { s := s₂, i := i₂ }) (eq : (s₁ s₂ : String) → (i₁ i₂ : Pos.Raw) → { s := s₂, i := i₂ }.hasNext = true → { s := s₁, i := i₁ }.hasNext = true → ¬Pos.Raw.get s₁ i₁ = Pos.Raw.get s₂ i₂ → motive { s := s₁, i := i₁ } { s := s₂, i := i₂ }) (base₁ : (s₁ s₂ : String) → (i₁ i₂ : Pos.Raw) → { s := s₂, i := i₂ }.hasNext = true → ¬{ s := s₁, i := i₁ }.hasNext = true → motive { s := s₁, i := i₁ } { s := s₂, i := i₂ }) (base₂ : (s₁ s₂ : String) → (i₁ i₂ : Pos.Raw) → ¬{ s := s₂, i := i₂ }.hasNext = true → motive { s := s₁, i := i₁ } { s := s₂, i := i₂ }) : motive it₁ it₂

Induction on String.ltb.

Equations

• One or more equations did not get rendered due to their size.

theorem String.ltb_cons_addChar' (c : Char) (s₁ s₂ : Legacy.Iterator) : ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c } { s := ofList (c :: s₂.s.toList), i := s₂.i + c } = ltb s₁ s₂

theorem String.ltb_cons_addChar (c : Char) (cs₁ cs₂ : List Char) (i₁ i₂ : Pos.Raw) : ltb { s := ofList (c :: cs₁), i := i₁ + c } { s := ofList (c :: cs₂), i := i₂ + c } = ltb { s := ofList cs₁, i := i₁ } { s := ofList cs₂, i := i₂ }

theorem String.lt_iff_toList_lt {s₁ s₂ : String} : s₁ < s₂ ↔ s₁.toList < s₂.toList

theorem String.lt_iff_ltb {s₁ s₂ : String} : s₁ < s₂ ↔ ltb (Legacy.iter s₁) (Legacy.iter s₂) = true

@[simp]

theorem String.head_empty : "".toList.head! = default

theorem String.le_iff_toList_le {s₁ s₂ : String} : s₁ ≤ s₂ ↔ s₁.toList ≤ s₂.toList

@[instance_reducible]

instance String.instLinearOrder : LinearOrder String

Equations

• One or more equations did not get rendered due to their size.

theorem String.ofList_eq {l : List Char} {s : String} : ofList l = s ↔ l = s.toList