Strings

Supplementary theorems about the String type.

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

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

Equations

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

instance String.LT' : LT String

Equations

• String.LT' = { lt := fun (s₁ s₂ : String) => String.ltb (String.iter s₁) (String.iter s₂) = true }

instance String.decidableLT : DecidableRel fun (x x_1 : String) => x < x_1

Equations

• String.decidableLT = id inferInstance

def String.ltb.inductionOn {motive : String.Iterator → String.Iterator → Sort u} (it₁ : String.Iterator) (it₂ : String.Iterator) (ind : (s₁ s₂ : String) → (i₁ i₂ : String.Pos) → String.Iterator.hasNext { s := s₂, i := i₂ } = true → String.Iterator.hasNext { s := s₁, i := i₁ } = true → String.get s₁ i₁ = String.get s₂ i₂ → motive (String.Iterator.next { s := s₁, i := i₁ }) (String.Iterator.next { s := s₂, i := i₂ }) → motive { s := s₁, i := i₁ } { s := s₂, i := i₂ }) (eq : (s₁ s₂ : String) → (i₁ i₂ : String.Pos) → String.Iterator.hasNext { s := s₂, i := i₂ } = true → String.Iterator.hasNext { s := s₁, i := i₁ } = true → ¬String.get s₁ i₁ = String.get s₂ i₂ → motive { s := s₁, i := i₁ } { s := s₂, i := i₂ }) (base₁ : (s₁ s₂ : String) → (i₁ i₂ : String.Pos) → String.Iterator.hasNext { s := s₂, i := i₂ } = true → ¬String.Iterator.hasNext { s := s₁, i := i₁ } = true → motive { s := s₁, i := i₁ } { s := s₂, i := i₂ }) (base₂ : (s₁ s₂ : String) → (i₁ i₂ : String.Pos) → ¬String.Iterator.hasNext { s := s₂, i := i₂ } = 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) (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₂ ↔ String.toList s₁ < String.toList s₂

instance String.LE : LE String

Equations

• String.LE = { le := fun (s₁ s₂ : String) => ¬s₂ < s₁ }

instance String.decidableLE : DecidableRel fun (x x_1 : String) => x ≤ x_1

Equations

• String.decidableLE = id inferInstance

@[simp]

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

theorem String.toList_inj {s₁ : String} {s₂ : String} : String.toList s₁ = String.toList s₂ ↔ s₁ = s₂

theorem String.nil_asString_eq_empty : List.asString [] = ""

@[simp]

theorem String.toList_empty : String.toList "" = []

theorem String.asString_inv_toList (s : String) : List.asString (String.toList s) = s

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

@[simp]

theorem String.head_empty : List.head! "".data = default

instance String.instLinearOrderString : LinearOrder String

Equations

• String.instLinearOrderString = LinearOrder.mk String.instLinearOrderString.proof_5 String.decidableLE decidableEqOfDecidableLE decidableLTOfDecidableLE

theorem List.toList_inv_asString (l : List Char) : String.toList (List.asString l) = l

@[simp]

theorem List.length_asString (l : List Char) : String.length (List.asString l) = List.length l

@[simp]

theorem List.asString_inj {l : List Char} {l' : List Char} : List.asString l = List.asString l' ↔ l = l'

@[simp]

theorem String.length_data (s : String) : List.length s.data = String.length s

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