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.all_set_next_of_lt (n : NFA.Unchecked.StateID) (s : NFA.Unchecked.State) (states : Array NFA.Unchecked.State) (h : n < states.size) (hn : s.nextOf < states.size) (hlt : ∀ (i : Nat) (x : i < states.size), states[i].nextOf < states.size) (i : Nat) (hi : i < states.size) :
      (states.set n s h)[i].nextOf < states.size
      source
      theorem Compiler.Lemmas.nextOfLt_of_union («from» to : Nat) (s : Array NFA.Unchecked.State) (alternates : Array NFA.Unchecked.StateID) (h1 : «from» < s.size) (h2 : to < s.size) (h3 : NextOfLt s) (hm : s[«from»] = NFA.Unchecked.State.Union alternates) :
      NextOfLt (s.set «from» (NFA.Unchecked.State.Union (alternates.push to)) h1)
      source
      theorem Compiler.Lemmas.nextOfLt_of_union_reverse («from» to : Nat) (s : Array NFA.Unchecked.State) (alternates : Array NFA.Unchecked.StateID) (h1 : «from» < s.size) (h2 : to < s.size) (h3 : NextOfLt s) (hm : s[«from»] = NFA.Unchecked.State.UnionReverse alternates) :
      NextOfLt (s.set «from» (NFA.Unchecked.State.UnionReverse (alternates.push to)) h1)