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.

@[simp]

theorem Regex.BufferStrategy.update_def {size : Nat} : (BufferStrategy size).Update = Buffer size

@[simp]

theorem Regex.BufferStrategy.empty_def {size : Nat} : (BufferStrategy size).empty = Buffer.empty

@[simp]

theorem Regex.BufferStrategy.write_def {size : Nat} {buffer : (BufferStrategy size).Update} {offset : Nat} {pos : String.Pos} : (BufferStrategy size).write buffer offset pos = Vector.setIfInBounds buffer offset (some pos)

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)] }

@[simp]

theorem Regex.HistoryStrategy.update_def : HistoryStrategy.Update = List (Nat × String.Pos)

@[simp]

theorem Regex.HistoryStrategy.empty_def : HistoryStrategy.empty = []

@[simp]

theorem Regex.HistoryStrategy.write_def {update : List (Nat × String.Pos)} {offset : Nat} {pos : String.Pos} : HistoryStrategy.write update offset pos = update ++ [(offset, pos)]