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.eat_lt («from» s : Nat) (n : NFA.Unchecked.StateID) (m : NFA.Unchecked.EatMode) (states : Array NFA.Unchecked.State) (h : «from» < states.size) (hmode : m.nextOf = s) (hm : states[«from»] = NFA.Unchecked.State.Eat m n) (hlt : states[«from»].nextOf < states.size) :
      s < states.size ∧ n < states.size
      source
      theorem Compiler.Lemmas.change_frame_step_lt («from» : Nat) (f t : NFA.Unchecked.StateID) (states : Array NFA.Unchecked.State) (h : «from» < states.size) (hm : states[«from»] = NFA.Unchecked.State.ChangeFrameStep f t) (hlt : states[«from»].nextOf < states.size) :
      f < states.size ∧ t < states.size
      source
      theorem Compiler.Lemmas.binary_union_lt («from» : Nat) (alt1 alt2 : NFA.Unchecked.StateID) (states : Array NFA.Unchecked.State) (h : «from» < states.size) (hm : states[«from»] = NFA.Unchecked.State.BinaryUnion alt1 alt2) (hlt : states[«from»].nextOf < states.size) :
      alt1 < states.size ∧ alt2 < states.size
      source
      theorem Compiler.Lemmas.union_lt («from» to : Nat) (alternates : Array NFA.Unchecked.StateID) (states : Array NFA.Unchecked.State) (h : «from» < states.size) (ht : to < states.size) (hm : states[«from»] = NFA.Unchecked.State.Union alternates) (hlt : states[«from»].nextOf < states.size) :
      List.maxD 0 (alternates.toList ++ [to]) < states.size
      source
      theorem Compiler.Lemmas.union_reverse_lt («from» to : Nat) (alternates : Array NFA.Unchecked.StateID) (states : Array NFA.Unchecked.State) (h : «from» < states.size) (ht : to < states.size) (hm : states[«from»] = NFA.Unchecked.State.UnionReverse alternates) (hlt : states[«from»].nextOf < states.size) :
      List.maxD 0 (alternates.toList ++ [to]) < states.size