Documentation

Regex.Data.String

@[simp]

theorem String.utf8Size.go_append (cs₁ cs₂ : List Char) :

utf8ByteSize.go (cs₁ ++ cs₂) = utf8ByteSize.go cs₁ + utf8ByteSize.go cs₂

@[simp]

theorem String.utf8Size.go_nil :

utf8ByteSize.go [] = 0

@[simp]

theorem String.utf8Size.go_cons (c : Char) (cs : List Char) :

utf8ByteSize.go (c :: cs) = utf8ByteSize.go cs + c.utf8Size

theorem String.next_le_endPosAux (p : Pos) (cs : List Char) (i ep : Pos) (lt : p < ep) (hep : ep = i + { byteIdx := utf8ByteSize.go cs }) :

p + utf8GetAux cs i p ≤ ep

theorem String.next_le_endPos (s : String) (p : Pos) (lt : p < s.endPos) :

s.next p ≤ s.endPos

def Char.isWordChar (ch : Char) :

Equations

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

Instances For

def String.Iterator.isCurrWord (it : Iterator) :

Equations

it.isCurrWord = (it.hasNext && it.curr.isWordChar)

Instances For

def String.Iterator.isPrevWord (it : Iterator) :

Equations

it.isPrevWord = (it.hasPrev && it.prev.curr.isWordChar)

Instances For

def String.Iterator.isAtWordBoundary (it : Iterator) :

Equations

it.isAtWordBoundary = (it.isCurrWord != it.isPrevWord)

Instances For

def String.Iterator.isAtNonWordBoundary (it : Iterator) :

Equations

it.isAtNonWordBoundary = (it.isCurrWord == it.isPrevWord)

Instances For

theorem String.Iterator.next'_eq_next (it : Iterator) (h : it.hasNext = true) :

it.next' h = it.next

theorem String.Iterator.next_toString (it : Iterator) :

it.next.toString = it.toString

theorem String.Iterator.next_le_endPos (it : Iterator) (h : it.hasNext = true) :

(it.next' h).pos ≤ (it.next' h).toString.endPos

theorem String.Iterator.lt_next (it : Iterator) :

it.pos < it.next.pos

theorem String.Iterator.next_le_four (it : Iterator) :

it.next.pos ≤ it.pos + { byteIdx := 4 }

@[simp]

theorem String.Iterator.next'_remainingBytes_lt {it : Iterator} {h : it.hasNext = true} :

(it.next' h).remainingBytes < it.remainingBytes

theorem String.Iterator.curr'_eq_curr {it : Iterator} {h : it.hasNext = true} :

it.curr' h = it.curr