structure Regex.Backtracker.StackEntry (σ : Strategy) (nfa : NFA) (startIdx maxIdx : Nat) : Type

• update : σ.Update
• state : Fin nfa.nodes.size
• it : Data.BoundedIterator startIdx maxIdx

def Regex.Backtracker.captureNextAux.pushNext (σ : Strategy) (nfa : NFA) (wf : nfa.WellFormed) (startIdx maxIdx : Nat) (stack : List (StackEntry σ nfa startIdx maxIdx)) (update : σ.Update) (state : Fin nfa.nodes.size) (it : Data.BoundedIterator startIdx maxIdx) : List (StackEntry σ nfa startIdx maxIdx)

Equations

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

@[irreducible]

def Regex.Backtracker.captureNextAux (σ : Strategy) (nfa : NFA) (wf : nfa.WellFormed) (startIdx maxIdx : Nat) (visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)) (stack : List (StackEntry σ nfa startIdx maxIdx)) : Option σ.Update × Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)

Equations

• One or more equations did not get rendered due to their size.
• Regex.Backtracker.captureNextAux σ nfa wf startIdx maxIdx visited [] = (none, visited)

def Regex.Backtracker.captureNext (σ : Strategy) (nfa : NFA) (wf : nfa.WellFormed) (it : String.Iterator) : Option σ.Update

Equations

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

@[irreducible]

def Regex.Backtracker.captureNext.go (σ : Strategy) (nfa : NFA) (wf : nfa.WellFormed) (startIdx maxIdx : Nat) (bit : Data.BoundedIterator startIdx maxIdx) (visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)) : Option σ.Update

Equations

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

def Regex.Backtracker.captureNextBuf (nfa : NFA) (wf : nfa.WellFormed) (bufferSize : Nat) (it : String.Iterator) : Option (Buffer bufferSize)

Equations

• Regex.Backtracker.captureNextBuf nfa wf bufferSize it = Regex.Backtracker.captureNext (Regex.BufferStrategy bufferSize) nfa wf it