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.

@[implicit_reducible]

instance String.LT' : LT String

This overrides an instance in core Lean.

@[implicit_reducible]

instance String.decidableLT' : DecidableLT String

This instance has a prime to avoid the name of the corresponding instance in core Lean.

@[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.

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₂ }

@[simp]

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

@[implicit_reducible]

instance String.LE : _root_.LE String

@[implicit_reducible]

instance String.decidableLE : DecidableLE String

@[simp]

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

@[deprecated String.ofList_nil (since := "2025-10-31")]

theorem String.asString_nil : ofList [] = ""

@[deprecated String.ofList_toList (since := "2025-10-31")]

theorem String.asString_toList (s : String) : ofList s.toList = s

theorem String.toList_nonempty {s : String} : s ≠ "" → s.toList = Legacy.front s :: (Legacy.drop s 1).toList

@[simp]

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

@[implicit_reducible]

instance String.instLinearOrder : LinearOrder String

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

@[deprecated String.toList_ofList (since := "2025-10-31")]

theorem List.toList_asString (l : List Char) : (String.ofList l).toList = l

@[deprecated String.ofList_eq (since := "2025-10-31")]

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