NFA

A byte oriented Thompson non-deterministic finite automaton (Checked.NFA), see also Tagged NFA.

def NFA.toCkecked (nfa : Unchecked.NFA) (captures : Array Capture) (groups : Array Nat) (hs : ∀ (i : Nat) (x : i < nfa.states.size), nfa.states[i].nextOf < nfa.states.size) (hv : Capture.valid captures) : Checked.NFA

transform Unchecked.NFA to Checked.NFA

Equations

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

structure Regex : Type

A compiled regular expression for searching Unicode haystacks.

• nfa : NFA.Checked.NFA

instance instToStringRegex : ToString Regex

Equations

• instToStringRegex = { toString := fun (m : Regex) => toString "" ++ toString m.nfa ++ toString "" }