def Regex.Strategy.refineUpdate {bufferSize : ℕ} (update : List (ℕ × String.Pos)) (buffer : Buffer bufferSize) : Prop

Equations

• Regex.Strategy.refineUpdate update buffer = (Regex.Strategy.materializeUpdates bufferSize update = buffer)

@[simp]

theorem Regex.Strategy.refineUpdate.empty {bufferSize : ℕ} : refineUpdate HistoryStrategy.empty (BufferStrategy bufferSize).empty

def Regex.Strategy.refineUpdateOpt {bufferSize : ℕ} : Option (List (ℕ × String.Pos)) → Option (Buffer bufferSize) → Prop

Equations

• Regex.Strategy.refineUpdateOpt none none = True
• Regex.Strategy.refineUpdateOpt (some update) (some buffer) = Regex.Strategy.refineUpdate update buffer
• Regex.Strategy.refineUpdateOpt x✝¹ x✝ = False

theorem Regex.Strategy.refineUpdateOpt.isSome_iff {bufferSize : ℕ} {matched' : Option (List (ℕ × String.Pos))} {matched : Option (Buffer bufferSize)} (h : refineUpdateOpt matched' matched) : matched'.isSome = true ↔ matched.isSome = true

theorem Regex.Strategy.refineUpdateOpt.none_iff {bufferSize : ℕ} {matched' : Option (List (ℕ × String.Pos))} {matched : Option (Buffer bufferSize)} (h : refineUpdateOpt matched' matched) : matched' = none ↔ matched = none

theorem Regex.Strategy.refineUpdateOpt.orElse {bufferSize : ℕ} {update₁ update₂ : Option (List (ℕ × String.Pos))} {buffer₁ buffer₂ : Option (Buffer bufferSize)} (h₁ : refineUpdateOpt update₁ buffer₁) (h₂ : refineUpdateOpt update₂ buffer₂) : refineUpdateOpt (update₁ <|> update₂) (buffer₁ <|> buffer₂)

def Regex.Strategy.refineUpdates {nfa : NFA} {bufferSize : ℕ} (updates : Vector (List (ℕ × String.Pos)) nfa.nodes.size) (buffers : Vector (Buffer bufferSize) nfa.nodes.size) : Prop

Equations

• Regex.Strategy.refineUpdates updates buffers = ∀ (i : Fin nfa.nodes.size), Regex.Strategy.refineUpdate updates[i] buffers[i]

theorem Regex.Strategy.refineUpdates.set_set {nfa : NFA} {bufferSize : ℕ} {updates : Vector (List (ℕ × String.Pos)) nfa.nodes.size} {buffers : Vector (Buffer bufferSize) nfa.nodes.size} {i : Fin nfa.nodes.size} {update : List (ℕ × String.Pos)} {buffer : Buffer bufferSize} (h₁ : refineUpdates updates buffers) (h₂ : refineUpdate update buffer) : refineUpdates (updates.set (↑i) update ⋯) (buffers.set (↑i) buffer ⋯)