structure Regex.Strategy : Type 1

• Update : Type
• empty : self.Update
• write : self.Update → Nat → String.Pos → self.Update

@[reducible, inline]

abbrev Regex.Buffer (size : Nat) : Type

Equations

• Regex.Buffer size = Vector (Option String.Pos) size

def Regex.Buffer.empty {size : Nat} : Buffer size

Equations

• Regex.Buffer.empty = Vector.replicate size none

def Regex.BufferStrategy (size : Nat) : Strategy

Equations

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

instance Regex.instReprUpdateBufferStrategy {size : Nat} : Repr (BufferStrategy size).Update

Equations

• Regex.instReprUpdateBufferStrategy = inferInstanceAs (Repr (Vector (Option String.Pos) size))

instance Regex.instInhabitedUpdateBufferStrategy {size : Nat} : Inhabited (BufferStrategy size).Update

Equations

• Regex.instInhabitedUpdateBufferStrategy = inferInstanceAs (Inhabited (Vector (Option String.Pos) size))

instance Regex.instDecidableEqUpdateBufferStrategy {size : Nat} : DecidableEq (BufferStrategy size).Update

Equations

• Regex.instDecidableEqUpdateBufferStrategy = inferInstanceAs (DecidableEq (Vector (Option String.Pos) size))

instance Regex.instGetElemUpdateBufferStrategyNatOptionPosLt {size : Nat} : GetElem (BufferStrategy size).Update Nat (Option String.Pos) fun (x : (BufferStrategy size).Update) (i : Nat) => i < size

Equations

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

def Regex.HistoryStrategy : Strategy

This strategy is inefficient and used only for proofs.

Equations

• Regex.HistoryStrategy = { Update := List (Nat × String.Pos), empty := [], write := fun (update : List (Nat × String.Pos)) (offset : Nat) (pos : String.Pos) => update ++ [(offset, pos)] }