Strings

Supplementary theorems about the String type.

@[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' : DecidableLT String

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.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₂ : Iterator) : ltb { s := mk (c :: s₁.s.data), i := s₁.i + c } { s := mk (c :: s₂.s.data), i := s₂.i + c } = ltb s₁ s₂

theorem String.ltb_cons_addChar (c : Char) (cs₁ cs₂ : List Char) (i₁ i₂ : Pos.Raw) : ltb { s := mk (c :: cs₁), i := i₁ + c } { s := mk (c :: cs₂), i := i₂ + c } = ltb { s := mk cs₁, i := i₁ } { s := mk 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 : DecidableLE String

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

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

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

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

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