Strings

Supplementary theorems about the String type.

@[simp]

theorem String.endPos_empty : "".endPos = 0

@[irreducible]

def String.ltb (s₁ s₂ : 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

instance String.LT' : LT String

This overrides an instance in core Lean.

Equations

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

instance String.decidableLT' : DecidableRel fun (x1 x2 : String) => x1 < x2

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

Equations

• String.decidableLT' = id inferInstance

@[irreducible]

def String.ltb.inductionOn {motive : Iterator → Iterator → Sort u} (it₁ it₂ : Iterator) (ind : (s₁ s₂ : String) → (i₁ i₂ : Pos) → { s := s₂, i := i₂ }.hasNext = true → { s := s₁, i := i₁ }.hasNext = true → s₁.get i₁ = s₂.get 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) → { 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₂ : Pos) → { 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) → ¬{ 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) (cs₁ cs₂ : List Char) (i₁ i₂ : Pos) : ltb { s := { data := c :: cs₁ }, i := i₁ + c } { s := { data := c :: cs₂ }, i := i₂ + c } = ltb { s := { data := cs₁ }, i := i₁ } { s := { data := cs₂ }, i := i₂ }

@[simp]

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

instance String.LE : _root_.LE String

Equations

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

instance String.decidableLE : DecidableRel fun (x1 x2 : String) => x1 ≤ x2

Equations

• String.decidableLE = id inferInstance

@[simp]

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

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

theorem String.asString_nil : [].asString = ""

@[deprecated String.asString_nil (since := "2024-06-04")]

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 (since := "2024-06-04")]

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

instance String.instLinearOrder : LinearOrder String

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 (since := "2024-06-04")]

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