Documentation

Mathlib.Data.String.Basic

Strings #

Supplementary theorems about the String type.

@[simp]
theorem String.endPos_empty :
"".endPos = 0
@[irreducible]

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

Equations
Instances For
    instance String.LT' :
    Equations
    instance String.decidableLT :
    DecidableRel fun (x1 x2 : String) => x1 < x2
    Equations
    @[irreducible]
    def String.ltb.inductionOn {motive : String.IteratorString.IteratorSort u} (it₁ : String.Iterator) (it₂ : String.Iterator) (ind : (s₁ s₂ : String) → (i₁ i₂ : String.Pos) → { s := s₂, i := i₂ }.hasNext = true{ s := s₁, i := i₁ }.hasNext = trues₁.get i₁ = s₂.get i₂motive { s := s₁, i := i₁ }.next { s := s₂, i := i₂ }.nextmotive { s := s₁, i := i₁ } { s := s₂, i := i₂ }) (eq : (s₁ s₂ : String) → (i₁ i₂ : String.Pos) → { s := s₂, i := i₂ }.hasNext = true{ s := s₁, i := i₁ }.hasNext = true¬s₁.get i₁ = s₂.get i₂motive { s := s₁, i := i₁ } { s := s₂, i := i₂ }) (base₁ : (s₁ s₂ : String) → (i₁ i₂ : String.Pos) → { s := s₂, i := i₂ }.hasNext = true¬{ s := s₁, i := i₁ }.hasNext = truemotive { s := s₁, i := i₁ } { s := s₂, i := i₂ }) (base₂ : (s₁ s₂ : String) → (i₁ i₂ : String.Pos) → ¬{ s := s₂, i := i₂ }.hasNext = truemotive { 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.
    Instances For
      theorem String.ltb_cons_addChar (c : Char) (cs₁ : List Char) (cs₂ : List Char) (i₁ : String.Pos) (i₂ : String.Pos) :
      String.ltb { s := { data := c :: cs₁ }, i := i₁ + c } { s := { data := c :: cs₂ }, i := i₂ + c } = String.ltb { s := { data := cs₁ }, i := i₁ } { s := { data := cs₂ }, i := i₂ }
      @[simp]
      theorem String.lt_iff_toList_lt {s₁ : String} {s₂ : String} :
      s₁ < s₂ s₁.toList < s₂.toList
      instance String.LE :
      Equations
      instance String.decidableLE :
      DecidableRel fun (x1 x2 : String) => x1 x2
      Equations
      @[simp]
      theorem String.le_iff_toList_le {s₁ : String} {s₂ : String} :
      s₁ s₂ s₁.toList s₂.toList
      theorem String.toList_inj {s₁ : String} {s₂ : String} :
      s₁.toList = s₂.toList s₁ = s₂
      theorem String.asString_nil :
      [].asString = ""
      @[deprecated String.asString_nil]
      theorem String.nil_asString_eq_empty :
      [].asString = ""

      Alias of String.asString_nil.

      @[simp]
      theorem String.toList_empty :
      "".toList = []
      theorem String.asString_toList (s : String) :
      s.toList.asString = s
      @[deprecated String.asString_toList]
      theorem String.asString_inv_toList (s : String) :
      s.toList.asString = s

      Alias of String.asString_toList.

      theorem String.toList_nonempty {s : String} :
      s ""s.toList = s.head :: (s.drop 1).toList
      @[simp]
      theorem String.head_empty :
      "".data.head! = default
      Equations
      • One or more equations did not get rendered due to their size.
      theorem List.toList_asString (l : List Char) :
      l.asString.toList = l
      @[deprecated List.toList_asString]
      theorem List.toList_inv_asString (l : List Char) :
      l.asString.toList = l

      Alias of List.toList_asString.

      @[simp]
      theorem List.length_asString (l : List Char) :
      l.asString.length = l.length
      @[simp]
      theorem List.asString_inj {l : List Char} {l' : List Char} :
      l.asString = l'.asString l = l'
      theorem List.asString_eq {l : List Char} {s : String} :
      l.asString = s l = s.toList
      @[simp]
      theorem String.length_data (s : String) :
      s.data.length = s.length