Documentation

Regex.Compiler.Patch

source
@[reducible, inline]
abbrev Compiler.Code.PatchM (α : Type) :
Type
Equations
Instances For
    source
    def Compiler.Code.patch («from» to : NFA.Unchecked.StateID) :
    PatchM Unit

    Add a transition from one state to another.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Compiler.Lemmas.patch_spec («from» : NFA.Unchecked.StateID) {to : NFA.Unchecked.StateID} {states : Array NFA.Unchecked.State} :
      ⦃fun (s : Array NFA.Unchecked.State) => s = states ∧ nextOfLt states ∧ «from» < states.size ∧ to < states.size⦄ Code.patch «from» to ⦃(fun (x : Unit) (r : Array NFA.Unchecked.State) => states.size = r.size ∧ to < r.size ∧ nextOfLt r, fun (x : String) => ⌜True⌝, ())⦄