Length-indexed input text.

structure Text (n : ℕ) : Type

Input to a parser. n is the number of bytes that haven't been consumed yet.

• bytes : ByteArray
• valid : n ≤ self.bytes.size

@[inline]

def Text.pos {n : ℕ} (t : Text n) : ℕ

Equations

• t.pos = t.bytes.size - n

theorem Text.pos_lt {n : ℕ} (t : Text (n + 1)) : t.pos < t.bytes.size

@[inline]

def Text.head {n : ℕ} (t : Text (n + 1)) : UInt8

Equations

• t.head = t.bytes[t.pos]

theorem Text.utf8Size_le {n : ℕ} {c : Char} (t : Text n) (h : t.bytes.utf8DecodeChar? t.pos = some c) : c.utf8Size ≤ n

def Text.ofString (s : String) : Text s.toUTF8.size

Equations

• Text.ofString s = { bytes := s.toUTF8, valid := ⋯ }

def Text.empty : Text 0

Equations

• Text.empty = { bytes := ByteArray.empty, valid := Text.empty._proof_1 }

@[inline]

def Text.dropTo {n : ℕ} (t : Text n) (m : ℕ) (h : m ≤ n) : Text m

Equations

• t.dropTo m h = { bytes := t.bytes, valid := ⋯ }

@[simp]

theorem Text.dropTo_self {n : ℕ} (t : Text n) (h : n ≤ n) : t.dropTo n h = t

@[simp]

theorem Text.dropTo_trans {n m k : ℕ} (t : Text n) (h : m ≤ n) (h' : k ≤ m) : (t.dropTo m h).dropTo k h' = t.dropTo k ⋯