def Char.isWordChar (ch : Char) : Bool

Equations

• ch.isWordChar = (ch.isAlphanum || decide (ch = '_'))

theorem String.Slice.Pos.le_of_not_lt {s : Slice} {p q : s.Pos} : ¬q < p → p ≤ q

theorem String.Slice.Pos.ne_endPos_of_lt {s : Slice} {p q : s.Pos} : p < q → p ≠ s.endPos

theorem String.Slice.Pos.next_le_of_lt {s : Slice} {p q : s.Pos} {h : p ≠ s.endPos} : p < q → p.next h ≤ q

theorem String.Slice.Pos.ofSlice_le_iff {s : String} {p : s.toSlice.Pos} {q : s.ValidPos} : p.ofSlice ≤ q ↔ p ≤ q.toSlice

@[simp]

theorem String.ValidPos.toSlice_lt_toSlice_iff {s : String} {p q : s.ValidPos} : p.toSlice < q.toSlice ↔ p < q

theorem String.ValidPos.next_le_of_lt {s : String} {p q : s.ValidPos} {h : p ≠ s.endValidPos} : p < q → p.next h ≤ q

def String.ValidPos.isCurrWord {s : String} (p : s.ValidPos) : Bool

Equations

• p.isCurrWord = if h : p ≠ s.endValidPos then (p.get h).isWordChar else false

def String.ValidPos.isPrevWord {s : String} (p : s.ValidPos) : Bool

Equations

• p.isPrevWord = if h : p ≠ s.startValidPos then ((p.prev h).get ⋯).isWordChar else false

def String.ValidPos.isAtWordBoundary {s : String} (p : s.ValidPos) : Bool

Equations

• p.isAtWordBoundary = (p.isCurrWord != p.isPrevWord)

def String.ValidPos.isAtNonWordBoundary {s : String} (p : s.ValidPos) : Bool

Equations

• p.isAtNonWordBoundary = (p.isCurrWord == p.isPrevWord)

@[irreducible, specialize #[]]

def String.ValidPos.find {s : String} (pos : s.ValidPos) (p : Char → Bool) : s.ValidPos

Equations

• pos.find p = if hn : pos = s.endValidPos then pos else if p (pos.get hn) = true then pos else (pos.next hn).find p

theorem String.ValidPos.ne_endValidPos_of_lt {s : String} {pos pos' : s.ValidPos} (lt : pos < pos') : pos ≠ s.endValidPos

@[simp]

theorem String.ValidPos.ne_next {s : String} {pos : s.ValidPos} {ne : pos ≠ s.endValidPos} : pos ≠ pos.next ne

@[irreducible]

def String.ValidPos.posRevInduction {s : String} {motive : s.ValidPos → Sort u} (endValidPos : motive s.endValidPos) (next : (p : s.ValidPos) → (h : p ≠ s.endValidPos) → motive (p.next h) → motive p) (p : s.ValidPos) : motive p

Equations

• String.ValidPos.posRevInduction endValidPos next p = if h : p = s.endValidPos then ⋯ ▸ endValidPos else next p h (String.ValidPos.posRevInduction endValidPos next (p.next h))

theorem String.ValidPos.splits_of_next {s l r : String} {p : s.ValidPos} {h : p ≠ s.endValidPos} (sp : (p.next h).Splits (l ++ singleton (p.get h)) r) : p.Splits l (singleton (p.get h) ++ r)

theorem String.ValidPos.splits_get_singleton {s l r : String} {c : Char} {p : s.ValidPos} (sp : p.Splits l (singleton c ++ r)) : p.get ⋯ = c

theorem String.ValidPos.lt_or_eq_of_le {s : String} {p p' : s.ValidPos} (le : p ≤ p') : p < p' ∨ p = p'

theorem String.ValidPos.Splits.exists_eq_append_left_of_lt {s l r : String} {p p' : s.ValidPos} (sp : p.Splits l r) (lt : p' < p) : ∃ (l₁ : String), ∃ (l₂ : String), l = l₁ ++ l₂ ∧ p'.Splits l₁ (l₂ ++ r)

theorem String.ValidPos.next_inj {s : String} {pos pos' : s.ValidPos} {h : pos ≠ s.endValidPos} {h' : pos' ≠ s.endValidPos} (eq : pos.next h = pos'.next h') : pos = pos'

theorem String.ValidPos.lt_of_le_of_ne {s : String} {pos pos' : s.ValidPos} (le : pos ≤ pos') (ne : pos ≠ pos') : pos < pos'

theorem String.ValidPos.le_of_lt_next {s : String} {pos pos' : s.ValidPos} {h' : pos' ≠ s.endValidPos} (lt : pos < pos'.next h') : pos ≤ pos'

theorem String.ValidPos.le_or_eq_of_le_next {s : String} {pos pos' : s.ValidPos} {h' : pos' ≠ s.endValidPos} (le : pos ≤ pos'.next h') : pos ≤ pos' ∨ pos = pos'.next h'

theorem String.ValidPos.le_next_iff {s : String} {pos pos' : s.ValidPos} {h' : pos' ≠ s.endValidPos} : pos ≤ pos'.next h' ↔ pos ≤ pos' ∨ pos = pos'.next h'

theorem String.ValidPos.lt_next_iff {s : String} {pos pos' : s.ValidPos} {h' : pos' ≠ s.endValidPos} : pos < pos'.next h' ↔ pos ≤ pos'

theorem String.ValidPos.le_iff_lt_or_eq {s : String} {pos pos' : s.ValidPos} : pos ≤ pos' ↔ pos < pos' ∨ pos = pos'

theorem String.ValidPos.lt_next_iff_lt_or_eq {s : String} {pos pos' : s.ValidPos} (h' : pos' ≠ s.endValidPos) : pos < pos'.next h' ↔ pos < pos' ∨ pos = pos'

structure String.ValidPosPlusOne (s : String) : Type

• offset : Pos.Raw
• isValidOrPlusOne : Pos.Raw.IsValid s self.offset ∨ self.offset = s.rawEndPos.offsetBy { byteIdx := 1 }

theorem String.ValidPosPlusOne.ext {s : String} {x y : s.ValidPosPlusOne} (offset : x.offset = y.offset) : x = y

theorem String.ValidPosPlusOne.ext_iff {s : String} {x y : s.ValidPosPlusOne} : x = y ↔ x.offset = y.offset

def String.instReprValidPosPlusOne.repr {s✝ : String} : s✝.ValidPosPlusOne → Nat → Std.Format

Equations

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

instance String.instReprValidPosPlusOne {s✝ : String} : Repr s✝.ValidPosPlusOne

Equations

• String.instReprValidPosPlusOne = { reprPrec := String.instReprValidPosPlusOne.repr }

def String.instDecidableEqValidPosPlusOne.decEq {s✝ : String} (x✝ x✝¹ : s✝.ValidPosPlusOne) : Decidable (x✝ = x✝¹)

Equations

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

instance String.instDecidableEqValidPosPlusOne {s✝ : String} : DecidableEq s✝.ValidPosPlusOne

Equations

• String.instDecidableEqValidPosPlusOne = String.instDecidableEqValidPosPlusOne.decEq

@[match_pattern]

def String.ValidPosPlusOne.validPos {s : String} (p : s.ValidPos) : s.ValidPosPlusOne

Equations

• String.ValidPosPlusOne.validPos p = { offset := p.offset, isValidOrPlusOne := ⋯ }

@[match_pattern]

def String.ValidPosPlusOne.sentinel (s : String) : s.ValidPosPlusOne

Equations

• String.ValidPosPlusOne.sentinel s = { offset := s.rawEndPos.offsetBy { byteIdx := 1 }, isValidOrPlusOne := ⋯ }

def String.ValidPosPlusOne.rec' {s : String} {motive : s.ValidPosPlusOne → Sort u} (validPos : (p : s.ValidPos) → motive (validPos p)) (sentinel : motive (sentinel s)) (p : s.ValidPosPlusOne) : motive p

Equations

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

instance String.ValidPosPlusOne.instInhabited {s : String} : Inhabited s.ValidPosPlusOne

Equations

• String.ValidPosPlusOne.instInhabited = { default := String.ValidPosPlusOne.validPos s.startValidPos }

@[inline]

def String.ValidPosPlusOne.isValid {s : String} (p : s.ValidPosPlusOne) : Bool

Equations

• p.isValid = decide (p.offset ≠ s.rawEndPos.offsetBy { byteIdx := 1 })

theorem String.ValidPosPlusOne.isValid_iff_isValid {s : String} (p : s.ValidPosPlusOne) : p.isValid = true ↔ Pos.Raw.IsValid s p.offset

def String.ValidPosPlusOne.asValidPos {s : String} (p : s.ValidPosPlusOne) (h : p.isValid = true) : s.ValidPos

Equations

• p.asValidPos h = { offset := p.offset, isValid := ⋯ }

def String.ValidPosPlusOne.lt {s : String} (p₁ p₂ : s.ValidPosPlusOne) : Prop

Equations

• p₁.lt p₂ = (p₁.offset < p₂.offset)

instance String.ValidPosPlusOne.instLT {s : String} : LT s.ValidPosPlusOne

Equations

• String.ValidPosPlusOne.instLT = { lt := String.ValidPosPlusOne.lt }

theorem String.ValidPosPlusOne.lt_iff {s : String} {p₁ p₂ : s.ValidPosPlusOne} : p₁ < p₂ ↔ p₁.offset < p₂.offset

instance String.ValidPosPlusOne.instDecidableLt {s : String} (p₁ p₂ : s.ValidPosPlusOne) : Decidable (p₁ < p₂)

Equations

• p₁.instDecidableLt p₂ = decidable_of_iff' (p₁.offset < p₂.offset) ⋯

def String.ValidPosPlusOne.next {s : String} (p : s.ValidPosPlusOne) (h : p.isValid = true) : s.ValidPosPlusOne

Equations

• p.next h = if h' : p.asValidPos h ≠ s.endValidPos then String.ValidPosPlusOne.validPos ((p.asValidPos h).next h') else String.ValidPosPlusOne.sentinel s

theorem String.ValidPosPlusOne.lt_sentinel_of_valid {s : String} {p : s.ValidPosPlusOne} (h : p.isValid = true) : p < sentinel s

@[simp]

theorem String.ValidPosPlusOne.lt_next {s : String} (p : s.ValidPosPlusOne) (h : p.isValid = true) : p < p.next h

def String.ValidPosPlusOne.remainingBytes {s : String} (p : s.ValidPosPlusOne) : Nat

Equations

• p.remainingBytes = s.rawEndPos.byteIdx + 1 - p.offset.byteIdx

theorem String.ValidPosPlusOne.lt_iff_remainingBytes_lt {s : String} {p₁ p₂ : s.ValidPosPlusOne} : p₁ < p₂ ↔ p₂.remainingBytes < p₁.remainingBytes

theorem String.ValidPosPlusOne.wellFounded_gt {s : String} : WellFounded fun (p q : s.ValidPosPlusOne) => q < p

instance String.ValidPosPlusOne.instWellFoundedRelation {s : String} : WellFoundedRelation s.ValidPosPlusOne

Equations

• String.ValidPosPlusOne.instWellFoundedRelation = { rel := fun (p q : s.ValidPosPlusOne) => q < p, wf := ⋯ }

def String.ValidPosPlusOne.le {s : String} (p₁ p₂ : s.ValidPosPlusOne) : Prop

Equations

• p₁.le p₂ = (p₁.offset ≤ p₂.offset)

instance String.ValidPosPlusOne.instLE {s : String} : LE s.ValidPosPlusOne

Equations

• String.ValidPosPlusOne.instLE = { le := String.ValidPosPlusOne.le }

theorem String.ValidPosPlusOne.le_iff {s : String} {p₁ p₂ : s.ValidPosPlusOne} : p₁ ≤ p₂ ↔ p₁.offset ≤ p₂.offset

@[simp]

theorem String.ValidPosPlusOne.validPos_le_validPos_iff {s : String} {p₁ p₂ : s.ValidPos} : validPos p₁ ≤ validPos p₂ ↔ p₁ ≤ p₂

instance String.ValidPosPlusOne.instDecidableLe {s : String} (p₁ p₂ : s.ValidPosPlusOne) : Decidable (p₁ ≤ p₂)

Equations

• p₁.instDecidableLe p₂ = decidable_of_iff' (p₁.offset ≤ p₂.offset) ⋯

theorem String.ValidPosPlusOne.isValid_of_isValid_of_le {s : String} {p₁ p₂ : s.ValidPosPlusOne} (h : p₂.isValid = true) (le : p₁ ≤ p₂) : p₁.isValid = true

theorem String.ValidPosPlusOne.validPos_inj {s : String} {p₁ p₂ : s.ValidPos} (h : validPos p₁ = validPos p₂) : p₁ = p₂

def String.ValidPosPlusOne.or {s : String} (p₁ p₂ : s.ValidPosPlusOne) : s.ValidPosPlusOne

Equations

• p₁.or p₂ = if p₁.isValid = true then p₁ else p₂

def String.ValidPosPlusOne.orElse {s : String} (p₁ : s.ValidPosPlusOne) (p₂ : Unit → s.ValidPosPlusOne) : s.ValidPosPlusOne

Equations

• p₁.orElse p₂ = if p₁.isValid = true then p₁ else p₂ ()

instance String.ValidPosPlusOne.instOrElse {s : String} : OrElse s.ValidPosPlusOne

Equations

• String.ValidPosPlusOne.instOrElse = { orElse := String.ValidPosPlusOne.orElse }

@[simp]

theorem String.ValidPosPlusOne.orElse_eq_or {s : String} {p₁ : s.ValidPosPlusOne} {p₂ : Unit → s.ValidPosPlusOne} : p₁.orElse p₂ = p₁.or (p₂ ())

@[simp]

theorem String.ValidPosPlusOne.hOrElse_eq_orElse {s : String} {p₁ : s.ValidPosPlusOne} {p₂ : Unit → s.ValidPosPlusOne} : (p₁ <|> p₂ ()) = p₁.orElse p₂

@[simp]

theorem String.ValidPosPlusOne.or_valid {s : String} {p₁ p₂ : s.ValidPosPlusOne} (h : p₁.isValid = true) : p₁.or p₂ = p₁

@[simp]

theorem String.ValidPosPlusOne.or_not_valid {s : String} {p₁ p₂ : s.ValidPosPlusOne} (h : ¬p₁.isValid = true) : p₁.or p₂ = p₂

@[simp]

theorem String.ValidPosPlusOne.isValid_validPos {s : String} {p : s.ValidPos} : (validPos p).isValid = true

@[simp]

theorem String.ValidPosPlusOne.not_isValid_sentinel {s : String} : (sentinel s).isValid = false

@[simp]

theorem String.ValidPosPlusOne.sentinel_or {s : String} {p₁ p₂ : s.ValidPosPlusOne} (h : p₁ = sentinel s) : p₁.or p₂ = p₂

@[simp]

theorem String.ValidPosPlusOne.validPos_or {s : String} {p : s.ValidPos} {p₁ p₂ : s.ValidPosPlusOne} (h : p₁ = validPos p) : p₁.or p₂ = p₁

@[simp]

theorem String.ValidPosPlusOne.or_sentinel {s : String} {p₁ p₂ : s.ValidPosPlusOne} (h : p₂ = sentinel s) : p₁.or p₂ = p₁

theorem String.ValidPosPlusOne.validPos_ne_sentinel {s : String} {p : s.ValidPos} : validPos p ≠ sentinel s

@[simp]

theorem String.ValidPosPlusOne.or_self {s : String} {p : s.ValidPosPlusOne} : p.or p = p

@[simp]

theorem String.ValidPosPlusOne.asValidPos_validPos {s : String} {p : s.ValidPos} : (validPos p).asValidPos ⋯ = p

@[simp]

theorem String.ValidPosPlusOne.validPos_asValidPos {s : String} {p : s.ValidPosPlusOne} {h : p.isValid = true} : validPos (p.asValidPos h) = p

def String.startValidPosPlusOne (s : String) : s.ValidPosPlusOne

Equations

• s.startValidPosPlusOne = String.ValidPosPlusOne.validPos s.startValidPos