structure Regex.Backtracker.StackEntry {s : String} (σ : Strategy s) (nfa : NFA) (startPos : s.ValidPos) : Type

• update : σ.Update
• state : Fin nfa.nodes.size
• pos : Data.BVPos startPos

def Regex.Backtracker.captureNextAux.pushNext {s : String} (σ : Strategy s) (nfa : NFA) (wf : nfa.WellFormed) (startPos : s.ValidPos) (stack : List (StackEntry σ nfa startPos)) (update : σ.Update) (state : Fin nfa.nodes.size) (pos : Data.BVPos startPos) : List (StackEntry σ nfa startPos)

Equations

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

@[irreducible]

def Regex.Backtracker.captureNextAux {s : String} (σ : Strategy s) (nfa : NFA) (wf : nfa.WellFormed) (startPos : s.ValidPos) (visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) (stack : List (StackEntry σ nfa startPos)) : Option σ.Update × Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)

Equations

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

def Regex.Backtracker.captureNext {s : String} (σ : Strategy s) (nfa : NFA) (wf : nfa.WellFormed) (startPos : s.ValidPos) : Option σ.Update

Equations

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

@[irreducible]

def Regex.Backtracker.captureNext.go {s : String} (σ : Strategy s) (nfa : NFA) (wf : nfa.WellFormed) (startPos : s.ValidPos) (pos : Data.BVPos startPos) (visited : Data.BitMatrix nfa.nodes.size (startPos.remainingBytes + 1)) : Option σ.Update

Equations

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

def Regex.Backtracker.captureNextBuf {s : String} (nfa : NFA) (wf : nfa.WellFormed) (bufferSize : Nat) (p : s.ValidPos) : Option (Buffer s bufferSize)

Equations

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