Documentation

Regex.Data.String

def Char.isWordChar (ch : Char) :

Equations

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

Instances For

def Regex.Data.String.isCurrWord {s : String} (p : s.Pos) :

Equations

Regex.Data.String.isCurrWord p = if h : p ≠ s.endPos then (p.get h).isWordChar else false

Instances For

def Regex.Data.String.isPrevWord {s : String} (p : s.Pos) :

Equations

Regex.Data.String.isPrevWord p = if h : p ≠ s.startPos then ((p.prev h).get ⋯).isWordChar else false

Instances For

def Regex.Data.String.isAtWordBoundary {s : String} (p : s.Pos) :

Equations

Regex.Data.String.isAtWordBoundary p = (Regex.Data.String.isCurrWord p != Regex.Data.String.isPrevWord p)

Instances For

def Regex.Data.String.isAtNonWordBoundary {s : String} (p : s.Pos) :

Equations

Regex.Data.String.isAtNonWordBoundary p = (Regex.Data.String.isCurrWord p == Regex.Data.String.isPrevWord p)

Instances For

@[irreducible, specialize #[]]

def Regex.Data.String.find {s : String} (pos : s.Pos) (p : Char → Bool) :

Equations

Regex.Data.String.find pos p = if hn : pos = s.endPos then pos else if p (pos.get hn) = true then pos else Regex.Data.String.find (pos.next hn) p

Instances For

theorem String.Pos.ne_endPos_of_lt {s : String} {pos pos' : s.Pos} (lt : pos < pos') :

pos ≠ s.endPos

@[simp]

theorem String.Pos.ne_next {s : String} {pos : s.Pos} {ne : pos ≠ s.endPos} :

pos ≠ pos.next ne

@[irreducible]

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

motive p

Equations

String.Pos.posRevInduction endPos next p = if h : p = s.endPos then ⋯ ▸ endPos else next p h (String.Pos.posRevInduction endPos next (p.next h))

Instances For

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

p.Splits l (singleton (p.get h) ++ r)

theorem String.Pos.splits_get_singleton {s l r : String} {c : Char} {p : s.Pos} (sp : p.Splits l (singleton c ++ r)) :

p.get ⋯ = c

theorem String.Pos.lt_or_eq_of_le {s : String} {p p' : s.Pos} (le : p ≤ p') :

p < p' ∨ p = p'

theorem String.Pos.Splits.exists_eq_append_left_of_lt {s l r : String} {p p' : s.Pos} (sp : p.Splits l r) (lt : p' < p) :

∃ (l₁ : String ), ∃ (l₂ : String ), l = l₁ ++ l₂ ∧ p'.Splits l₁ (l₂ ++ r)

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

pos = pos'

theorem String.Pos.le_of_lt_next {s : String} {pos pos' : s.Pos} {h' : pos' ≠ s.endPos} (lt : pos < pos'.next h') :

pos ≤ pos'

theorem String.Pos.le_or_eq_of_le_next {s : String} {pos pos' : s.Pos} {h' : pos' ≠ s.endPos} (le : pos ≤ pos'.next h') :

pos ≤ pos' ∨ pos = pos'.next h'

theorem String.Pos.le_next_iff {s : String} {pos pos' : s.Pos} {h' : pos' ≠ s.endPos} :

pos ≤ pos'.next h' ↔ pos ≤ pos' ∨ pos = pos'.next h'

theorem String.Pos.lt_next_iff {s : String} {pos pos' : s.Pos} {h' : pos' ≠ s.endPos} :

pos < pos'.next h' ↔ pos ≤ pos'

theorem String.Pos.le_iff_lt_or_eq {s : String} {pos pos' : s.Pos} :

pos ≤ pos' ↔ pos < pos' ∨ pos = pos'

theorem String.Pos.lt_next_iff_lt_or_eq {s : String} {pos pos' : s.Pos} (h' : pos' ≠ s.endPos) :

pos < pos'.next h' ↔ pos < pos' ∨ pos = pos'

structure String.PosPlusOne (s : String) :

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

Instances For

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

x = y

theorem String.PosPlusOne.ext_iff {s : String} {x y : s.PosPlusOne} :

x = y ↔ x.offset = y.offset

def String.instReprPosPlusOne.repr {s✝ : String} :

s✝.PosPlusOne → Nat → Std.Format

Equations

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

Instances For

instance String.instReprPosPlusOne {s✝ : String} :

Repr s✝.PosPlusOne

Equations

String.instReprPosPlusOne = { reprPrec := String.instReprPosPlusOne.repr }

def String.instDecidableEqPosPlusOne.decEq {s✝ : String} (x✝ x✝¹ : s✝.PosPlusOne) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

instance String.instDecidableEqPosPlusOne {s✝ : String} :

DecidableEq s✝.PosPlusOne

Equations

String.instDecidableEqPosPlusOne = String.instDecidableEqPosPlusOne.decEq

@[match_pattern]

def String.PosPlusOne.pos {s : String} (p : s.Pos) :

Equations

String.PosPlusOne.pos p = { offset := p.offset, isValidOrPlusOne := ⋯ }

Instances For

@[match_pattern]

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

Equations

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

Instances For

def String.PosPlusOne.rec' {s : String} {motive : s.PosPlusOne → Sort u} (pos : (p : s.Pos) → motive (pos p)) (sentinel : motive (sentinel s)) (p : s.PosPlusOne) :

motive p

Equations

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

Instances For

instance String.PosPlusOne.instInhabited {s : String} :

Inhabited s.PosPlusOne

Equations

String.PosPlusOne.instInhabited = { default := String.PosPlusOne.pos s.startPos }

@[inline]

def String.PosPlusOne.isValid {s : String} (p : s.PosPlusOne) :

Equations

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

Instances For

theorem String.PosPlusOne.isValid_iff_isValid {s : String} (p : s.PosPlusOne) :

p.isValid = true ↔ Pos.Raw.IsValid s p.offset

def String.PosPlusOne.asPos {s : String} (p : s.PosPlusOne) (h : p.isValid = true) :

Equations

p.asPos h = { offset := p.offset, isValid := ⋯ }

Instances For

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

Equations

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

Instances For

instance String.PosPlusOne.instLT {s : String} :

LT s.PosPlusOne

Equations

String.PosPlusOne.instLT = { lt := String.PosPlusOne.lt }

theorem String.PosPlusOne.lt_iff {s : String} {p₁ p₂ : s.PosPlusOne} :

p₁ < p₂ ↔ p₁.offset < p₂.offset

instance String.PosPlusOne.instDecidableLt {s : String} (p₁ p₂ : s.PosPlusOne) :

Decidable (p₁ < p₂)

Equations

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

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

Equations

p.next h = if h' : p.asPos h ≠ s.endPos then String.PosPlusOne.pos ((p.asPos h).next h') else String.PosPlusOne.sentinel s

Instances For

theorem String.PosPlusOne.lt_sentinel_of_valid {s : String} {p : s.PosPlusOne} (h : p.isValid = true) :

@[simp]

theorem String.PosPlusOne.lt_next {s : String} (p : s.PosPlusOne) (h : p.isValid = true) :

p < p.next h

def String.PosPlusOne.remainingBytes {s : String} (p : s.PosPlusOne) :

Equations

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

Instances For

theorem String.PosPlusOne.lt_iff_remainingBytes_lt {s : String} {p₁ p₂ : s.PosPlusOne} :

p₁ < p₂ ↔ p₂.remainingBytes < p₁.remainingBytes

theorem String.PosPlusOne.wellFounded_gt {s : String} :

WellFounded fun (p q : s.PosPlusOne) => q < p

instance String.PosPlusOne.instWellFoundedRelation {s : String} :

WellFoundedRelation s.PosPlusOne

Equations

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

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

Equations

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

Instances For

instance String.PosPlusOne.instLE {s : String} :

LE s.PosPlusOne

Equations

String.PosPlusOne.instLE = { le := String.PosPlusOne.le }

theorem String.PosPlusOne.le_iff {s : String} {p₁ p₂ : s.PosPlusOne} :

p₁ ≤ p₂ ↔ p₁.offset ≤ p₂.offset

@[simp]

theorem String.PosPlusOne.pos_le_pos_iff {s : String} {p₁ p₂ : s.Pos} :

pos p₁ ≤ pos p₂ ↔ p₁ ≤ p₂

instance String.PosPlusOne.instDecidableLe {s : String} (p₁ p₂ : s.PosPlusOne) :

Decidable (p₁ ≤ p₂)

Equations

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

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

p₁.isValid = true

theorem String.PosPlusOne.pos_inj {s : String} {p₁ p₂ : s.Pos} (h : pos p₁ = pos p₂) :

p₁ = p₂

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

Equations

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

Instances For

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

Equations

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

Instances For

instance String.PosPlusOne.instOrElse {s : String} :

OrElse s.PosPlusOne

Equations

String.PosPlusOne.instOrElse = { orElse := String.PosPlusOne.orElse }

@[simp]

theorem String.PosPlusOne.orElse_eq_or {s : String} {p₁ : s.PosPlusOne} {p₂ : Unit → s.PosPlusOne} :

p₁.orElse p₂ = p₁.or (p₂ ())

@[simp]

theorem String.PosPlusOne.hOrElse_eq_orElse {s : String} {p₁ : s.PosPlusOne} {p₂ : Unit → s.PosPlusOne} :

(p₁ <|> p₂ ()) = p₁.orElse p₂

@[simp]

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

p₁.or p₂ = p₁

@[simp]

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

p₁.or p₂ = p₂

@[simp]

theorem String.PosPlusOne.isValid_pos {s : String} {p : s.Pos} :

(pos p).isValid = true

@[simp]

theorem String.PosPlusOne.not_isValid_sentinel {s : String} :

(sentinel s).isValid = false

@[simp]

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

p₁.or p₂ = p₂

@[simp]

theorem String.PosPlusOne.pos_or {s : String} {p : s.Pos} {p₁ p₂ : s.PosPlusOne} (h : p₁ = pos p) :

p₁.or p₂ = p₁

@[simp]

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

p₁.or p₂ = p₁

theorem String.PosPlusOne.pos_ne_sentinel {s : String} {p : s.Pos} :

pos p ≠ sentinel s

@[simp]

theorem String.PosPlusOne.or_self {s : String} {p : s.PosPlusOne} :

p.or p = p

@[simp]

theorem String.PosPlusOne.asPos_pos {s : String} {p : s.Pos} :

(pos p).asPos ⋯ = p

@[simp]

theorem String.PosPlusOne.pos_asPos {s : String} {p : s.PosPlusOne} {h : p.isValid = true} :

pos (p.asPos h) = p

def String.startPosPlusOne (s : String) :

Equations

s.startPosPlusOne = String.PosPlusOne.pos s.startPos

Instances For