structure Regex.Data.BoundedIterator (startIdx maxIdx : Nat) : Type

• it : String.Iterator
• ge : startIdx ≤ self.it.pos.byteIdx
• le : self.it.pos.byteIdx ≤ maxIdx
• eq : maxIdx = self.it.toString.endPos.byteIdx

theorem Regex.Data.BoundedIterator.ext {startIdx maxIdx : Nat} {x y : BoundedIterator startIdx maxIdx} (it : x.it = y.it) : x = y

theorem Regex.Data.BoundedIterator.ext_iff {startIdx maxIdx : Nat} {x y : BoundedIterator startIdx maxIdx} : x = y ↔ x.it = y.it

def Regex.Data.BoundedIterator.toString {startIdx maxIdx : Nat} (bit : BoundedIterator startIdx maxIdx) : String

Equations

• bit.toString = bit.it.toString

def Regex.Data.BoundedIterator.pos {startIdx maxIdx : Nat} (bit : BoundedIterator startIdx maxIdx) : String.Pos

Equations

• bit.pos = bit.it.pos

def Regex.Data.BoundedIterator.index {startIdx maxIdx : Nat} (bit : BoundedIterator startIdx maxIdx) : Fin (maxIdx + 1 - startIdx)

Equations

• bit.index = ⟨bit.it.pos.byteIdx - startIdx, ⋯⟩

def Regex.Data.BoundedIterator.hasNext {startIdx maxIdx : Nat} (bit : BoundedIterator startIdx maxIdx) : Bool

Equations

• bit.hasNext = bit.it.hasNext

def Regex.Data.BoundedIterator.next {startIdx maxIdx : Nat} (bit : BoundedIterator startIdx maxIdx) (h : bit.hasNext = true) : BoundedIterator startIdx maxIdx

Equations

• bit.next h = { it := bit.it.next' h, ge := ⋯, le := ⋯, eq := ⋯ }

def Regex.Data.BoundedIterator.nextn {startIdx maxIdx : Nat} (bit : BoundedIterator startIdx maxIdx) (n : Nat) : BoundedIterator startIdx maxIdx

Equations

• bit.nextn 0 = bit
• bit.nextn n_2.succ = if h : bit.hasNext = true then (bit.next h).nextn n_2 else bit

def Regex.Data.BoundedIterator.toEnd {startIdx maxIdx : Nat} (bit : BoundedIterator startIdx maxIdx) : BoundedIterator startIdx maxIdx

Equations

• bit.toEnd = { it := bit.it.toEnd, ge := ⋯, le := ⋯, eq := ⋯ }

def Regex.Data.BoundedIterator.curr {startIdx maxIdx : Nat} (bit : BoundedIterator startIdx maxIdx) (h : bit.hasNext = true) : Char

Equations

• bit.curr h = bit.it.curr' h

def Regex.Data.BoundedIterator.remainingBytes {startIdx maxIdx : Nat} (bit : BoundedIterator startIdx maxIdx) : Nat

Equations

• bit.remainingBytes = bit.it.remainingBytes

theorem Regex.Data.BoundedIterator.next_remainingBytes_lt {startIdx maxIdx : Nat} (bit : BoundedIterator startIdx maxIdx) (h : bit.hasNext = true) : (bit.next h).remainingBytes < bit.remainingBytes

def Regex.Data.BoundedIterator.Valid {startIdx maxIdx : Nat} (bit : BoundedIterator startIdx maxIdx) : Prop

Equations

• bit.Valid = (String.Pos.isValid bit.it.toString bit.it.pos = true)