@[reducible, inline]

abbrev NFA.PatternID : Type

The identifier of a regex pattern, represented by a Nat

Equations

• NFA.PatternID = Nat

inductive NFA.Capture.Role : Type

• Start : Role
• End : Role

instance NFA.Capture.instBEqRole : BEq Role

Equations

• NFA.Capture.instBEqRole = { beq := NFA.Capture.beqRole✝ }

instance NFA.Capture.instDecidableEqRole : DecidableEq Role

Equations

• NFA.Capture.instDecidableEqRole x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance NFA.Capture.instLawfulBEqRole : LawfulBEq Role

instance NFA.Capture.instReflBEqRole : ReflBEq Role

def NFA.Capture.toSlot (role : Role) (group : Nat) : Nat

Equations

• NFA.Capture.toSlot NFA.Capture.Role.Start group = group * 2
• NFA.Capture.toSlot NFA.Capture.Role.End group = group * 2 + 1

def NFA.Capture.IsValid (role : Role) (group slot : Nat) : Prop

Equations

• NFA.Capture.IsValid NFA.Capture.Role.Start group slot = (group * 2 = slot)
• NFA.Capture.IsValid NFA.Capture.Role.End group slot = (group * 2 + 1 = slot)

def NFA.Capture.toString : Role → String

Equations

• NFA.Capture.toString NFA.Capture.Role.Start = toString "Start"
• NFA.Capture.toString NFA.Capture.Role.End = toString "End"

instance NFA.Capture.instToStringRole : ToString Role

Equations

• NFA.Capture.instToStringRole = { toString := NFA.Capture.toString }

structure NFA.Capture : Type

A capture location. slot in this context refers to the specific capture group slot offset that is being recorded. Each capturing group has two slots corresponding to the start and end of the matching portion of that group.

• role : Role
• group : Nat
• slot : Nat
• isValid : IsValid self.role self.group self.slot

theorem NFA.Capture.ext_iff {x y : Capture} : x = y ↔ x.role = y.role ∧ x.group = y.group ∧ x.slot = y.slot

theorem NFA.Capture.ext {x y : Capture} (role : x.role = y.role) (group : x.group = y.group) (slot : x.slot = y.slot) : x = y

@[reducible, inline]

abbrev NFA.Capture.SlotGroup : Type

Equations

• NFA.Capture.SlotGroup = (Nat × Nat)

def NFA.Capture.toSlots (captures : Array Capture) : Array SlotGroup

Transform captures to a sorted array of (slot, group) tuples.

Equations

• NFA.Capture.toSlots captures = ((Array.map NFA.Capture.toSlots.f captures).mergeSort NFA.Capture.toSlots.le).unique

def NFA.Capture.toSlots.f (c : Capture) : Nat × Nat

Equations

• NFA.Capture.toSlots.f c = (c.slot, c.group)

def NFA.Capture.toSlots.le (a b : SlotGroup) : Bool

Equations

• NFA.Capture.toSlots.le a b = decide (a.fst ≤ b.fst)

def NFA.Capture.valid (captures : Array Capture) : Prop

A valid capture array consists of capture groups with two slots. For every capture group slot with Role.End exists a group slot with Role.Start

Equations

• One or more equations did not get rendered due to their size.

def NFA.Slots.Valid (slots : Array Capture.SlotGroup) : Prop

A valid slot array of (slot, group) tuples consists of groups with two slots at consecutive positions. The groups are not always consecutive, i.e. regex '(a){0}(a)' with slots #[(0, 0), (1, 0), (4, 2), (5, 2)]

Equations

• One or more equations did not get rendered due to their size.

inductive NFA.Look : Type

The high-level intermediate representation for a look-around assertion.

• Start : Look

  Match the beginning of text.

• End : Look

  Match the end of text.

• EndWithOptionalLF : Look

  Match the end of text (before optional newline).

• StartLF : Look

  Match the beginning of a line or the beginning of text.

• EndLF : Look

  Match of a line or the end of text.

• StartCRLF : Look

  Match the beginning of a line or the beginning of text.

• EndCRLF : Look

  Match of a line or the end of text.

• WordUnicode : Look

  Match a Unicode-aware word boundary.

• WordUnicodeNegate : Look

  Match a Unicode-aware negation of a word boundary.

• WordStartUnicode : Look

  Match the start of a Unicode word boundary.

• WordEndUnicode : Look

  Match the end of a Unicode word boundary.

• WordStartHalfUnicode : Look

  Match the start half of a Unicode word boundary.

• WordEndHalfUnicode : Look

  Match the end half of a Unicode word boundary.

• PreviousMatch : Look

  Match the end of the previous match or start of string

• ClearMatches : Look

  Clear matches

instance NFA.instBEqLook : BEq Look

Equations

• NFA.instBEqLook = { beq := NFA.beqLook✝ }

instance NFA.instDecidableEqLook : DecidableEq Look

Equations

• NFA.instDecidableEqLook x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

def NFA.Look.toString : Look → String

Equations

• NFA.Look.Start.toString = toString "Start"
• NFA.Look.End.toString = toString "End"
• NFA.Look.EndWithOptionalLF.toString = toString "EndWithOptionalLF"
• NFA.Look.StartLF.toString = toString "StartLF"
• NFA.Look.EndLF.toString = toString "EndLF"
• NFA.Look.StartCRLF.toString = toString "StartCRLF"
• NFA.Look.EndCRLF.toString = toString "EndCRLF"
• NFA.Look.WordUnicode.toString = toString "WordUnicode"
• NFA.Look.WordUnicodeNegate.toString = toString "WordUnicodeNegate"
• NFA.Look.WordStartUnicode.toString = toString "WordStartUnicode"
• NFA.Look.WordEndUnicode.toString = toString "WordEndUnicode"
• NFA.Look.WordStartHalfUnicode.toString = toString "WordStartHalfUnicode"
• NFA.Look.WordEndHalfUnicode.toString = toString "WordEndHalfUnicode"
• NFA.Look.PreviousMatch.toString = toString "PreviousMatch"
• NFA.Look.ClearMatches.toString = toString "ClearMatches"

instance NFA.instToStringLook : ToString Look

Equations

• NFA.instToStringLook = { toString := NFA.Look.toString }

@[reducible, inline]

abbrev NFA.Unchecked.StateID : Type

The identifier of a finite automaton state, represented by a Nat. The identifier may refer to a non existing state.

Equations

• NFA.Unchecked.StateID = Nat

inductive NFA.Unchecked.EatMode : Type

• Until : StateID → EatMode

  Eat frames until State found

• ToLast : StateID → EatMode

  Eat frames inclusive last occurunce of State.

instance NFA.Unchecked.instBEqEatMode : BEq EatMode

Equations

• NFA.Unchecked.instBEqEatMode = { beq := NFA.Unchecked.beqEatMode✝ }

instance NFA.Unchecked.instDecidableEqEatMode : DecidableEq EatMode

Equations

• NFA.Unchecked.instDecidableEqEatMode = NFA.Unchecked.decEqEatMode✝

def NFA.Unchecked.EatMode.toString : EatMode → String

Equations

• (NFA.Unchecked.EatMode.Until sid).toString = toString "Until " ++ toString sid ++ toString ""
• (NFA.Unchecked.EatMode.ToLast sid).toString = toString "ToLast " ++ toString sid ++ toString ""

def NFA.Unchecked.EatMode.nextOf (m : EatMode) : Nat

Equations

• (NFA.Unchecked.EatMode.Until sid).nextOf = sid
• (NFA.Unchecked.EatMode.ToLast sid).nextOf = sid

instance NFA.Unchecked.instToStringEatMode : ToString EatMode

Equations

• NFA.Unchecked.instToStringEatMode = { toString := NFA.Unchecked.EatMode.toString }

structure NFA.Unchecked.Transition : Type

A single transition to another state. This transition may only be followed if the current char in the haystack falls in the inclusive range of chars specified.

• start : UInt32

  The inclusive start of the char range.

• end : UInt32

  The inclusive end of the char range.

• next : StateID

  The identifier of the state to transition to.

instance NFA.Unchecked.instBEqTransition : BEq Transition

Equations

• NFA.Unchecked.instBEqTransition = { beq := NFA.Unchecked.beqTransition✝ }

instance NFA.Unchecked.instDecidableEqTransition : DecidableEq Transition

Equations

• NFA.Unchecked.instDecidableEqTransition = NFA.Unchecked.decEqTransition✝

def NFA.Unchecked.Transition.matches (trans : Transition) (c : Char) : Bool

check if c falls in the inclusive range of chars specified in Transition trans

Equations

• trans.matches c = (decide (trans.start ≤ c.val) && decide (c.val ≤ trans.end))

inductive NFA.Unchecked.State : Type

A state in an NFA.

• Empty (next : StateID) : State

  An empty state whose only purpose is to forward the automaton to another state via an unconditional epsilon transition.

• NextChar (offset : Nat) (next : StateID) : State

  use next char

• Fail : State

  Fail, force backtrack

• Eat (mode : EatMode) (next : StateID) : State

  remove Frame.Step in stack

• ChangeFrameStep («from» to : StateID) : State

  change Frame.Step in stack and force backtrack

• RemoveFrameStep (sid : StateID) : State

  remove Frame.Step in stack and force backtrack

• BackRef (n : Nat) (case_insensitive : Bool) (sid : StateID) : State

  A state with a single transition may only be followed if the currunt chars match the backrefence to the capturung group.

• ByteRange (trans : Transition) : State

  A state with a single transition that can only be taken if the current input symbol is in a particular range of chars.

• SparseTransitions (transitions : Array Transition) : State

  A sequence of transitions used to represent a sparse state.

• Look (look : NFA.Look) (next : StateID) : State

  A conditional epsilon transition satisfied via some sort of look-around.

• Union (alternates : Array StateID) : State

  An alternation such that there exists an epsilon transition to all states in alternates, where matches found via earlier transitions are preferred over later transitions.

• UnionReverse (alternates : Array StateID) : State

  An alternation such that there exists an epsilon transition to all states in alternates, where matches found via later transitions are preferred over earlier transitions.

• BinaryUnion (alt1 alt2 : StateID) : State

  An alternation such that there exists precisely two unconditional epsilon transitions

• Capture (role : Capture.Role) (next : StateID) (pattern_id : PatternID) (group slot : Nat) (isValid : Capture.IsValid role group slot) : State

  An empty state that records a capture location. slot in this context refers to the specific capture group slot offset that is being recorded. Each capturing group has two slots corresponding to the start and end of the matching portion of that group.

• Match (pattern_id : PatternID) : State

  A match state. There is at least one such occurrence of this state for each regex that can match that is in this NFA.

instance NFA.Unchecked.instBEqState : BEq State

Equations

• NFA.Unchecked.instBEqState = { beq := NFA.Unchecked.beqState✝ }

instance NFA.Unchecked.instDecidableEqState : DecidableEq State

Equations

• NFA.Unchecked.instDecidableEqState = NFA.Unchecked.decEqState✝

instance NFA.Unchecked.instBEqState_1 : BEq State

Equations

• NFA.Unchecked.instBEqState_1 = { beq := NFA.Unchecked.beq'✝ }

def NFA.Unchecked.State.toString : State → String

Equations

• One or more equations did not get rendered due to their size.
• (NFA.Unchecked.State.Empty next).toString = toString "State.Empty => " ++ toString next ++ toString ""
• (NFA.Unchecked.State.NextChar offset next).toString = toString "State.NextChar offset " ++ toString offset ++ toString " => " ++ toString next ++ toString ""
• NFA.Unchecked.State.Fail.toString = toString "State.Fail"
• (NFA.Unchecked.State.Eat s n).toString = toString "State.Eat " ++ toString s ++ toString " => " ++ toString n ++ toString ""
• (NFA.Unchecked.State.ChangeFrameStep «from» to).toString = toString "State.ChangeFrameStep from " ++ toString «from» ++ toString " to " ++ toString to ++ toString ""
• (NFA.Unchecked.State.RemoveFrameStep sid).toString = toString "State.RemoveFrameStep " ++ toString sid ++ toString ""
• (NFA.Unchecked.State.Look look next).toString = toString "State.Look " ++ toString look ++ toString " => " ++ toString next ++ toString ""
• (NFA.Unchecked.State.BinaryUnion alt1 alt2).toString = toString "State.BinaryUnion(" ++ toString alt1 ++ toString ", " ++ toString alt2 ++ toString ")"
• (NFA.Unchecked.State.Match pattern_id).toString = toString "State.Match (" ++ toString pattern_id ++ toString ")"

def NFA.Unchecked.State.nextOf (s : State) : StateID

next StateID of State s

Equations

• (NFA.Unchecked.State.Empty next).nextOf = next
• (NFA.Unchecked.State.NextChar offset next).nextOf = next
• NFA.Unchecked.State.Fail.nextOf = 0
• (NFA.Unchecked.State.Eat (NFA.Unchecked.EatMode.Until s_2) next).nextOf = Nat.max s_2 next
• (NFA.Unchecked.State.Eat (NFA.Unchecked.EatMode.ToLast s_2) next).nextOf = Nat.max s_2 next
• (NFA.Unchecked.State.ChangeFrameStep f t).nextOf = Nat.max f t
• (NFA.Unchecked.State.RemoveFrameStep next).nextOf = next
• (NFA.Unchecked.State.BackRef n case_insensitive next).nextOf = next
• (NFA.Unchecked.State.ByteRange trans).nextOf = trans.next
• (NFA.Unchecked.State.SparseTransitions trans).nextOf = List.maxD 0 (Array.map (fun (x : NFA.Unchecked.Transition) => x.next) trans).toList
• (NFA.Unchecked.State.Look look next).nextOf = next
• (NFA.Unchecked.State.Union alts).nextOf = List.maxD 0 alts.toList
• (NFA.Unchecked.State.UnionReverse alts).nextOf = List.maxD 0 alts.toList
• (NFA.Unchecked.State.BinaryUnion alt1 alt2).nextOf = Nat.max alt1 alt2
• (NFA.Unchecked.State.Capture role next pattern_id group slot isValid).nextOf = next
• (NFA.Unchecked.State.Match pattern_id).nextOf = 0

instance NFA.Unchecked.instToStringState : ToString State

Equations

• NFA.Unchecked.instToStringState = { toString := NFA.Unchecked.State.toString }

structure NFA.Unchecked.NFA : Type

A char oriented Thompson non-deterministic finite automaton (NFA).

• states : Array State
• start_anchored : StateID
• start_unanchored : StateID

def NFA.Unchecked.NFA.toString (nfa : NFA) : String

Equations

• One or more equations did not get rendered due to their size.

instance NFA.instToStringNFA : ToString Unchecked.NFA

Equations

• NFA.instToStringNFA = { toString := NFA.Unchecked.NFA.toString }

inductive NFA.Checked.EatMode (n : Nat) : Type

• Until {n : Nat} : Fin n → EatMode n

  Eat frames until State found

• ToLast {n : Nat} : Fin n → EatMode n

  Eat frames inclusive last occurunce of State.

instance NFA.Checked.instBEqEatMode {n✝ : Nat} : BEq (EatMode n✝)

Equations

• NFA.Checked.instBEqEatMode = { beq := NFA.Checked.beqEatMode✝ }

instance NFA.Checked.instDecidableEqEatMode {n✝ : Nat} : DecidableEq (EatMode n✝)

Equations

• NFA.Checked.instDecidableEqEatMode = NFA.Checked.decEqEatMode✝

def NFA.Checked.EatMode.toString {n : Nat} : EatMode n → String

Equations

• (NFA.Checked.EatMode.Until sid).toString = toString "Until " ++ toString sid ++ toString ""
• (NFA.Checked.EatMode.ToLast sid).toString = toString "ToLast " ++ toString sid ++ toString ""

instance NFA.Checked.instToStringEatMode {n : Nat} : ToString (EatMode n)

Equations

• NFA.Checked.instToStringEatMode = { toString := NFA.Checked.EatMode.toString }

structure NFA.Checked.Transition (n : Nat) : Type

A single transition to another state. This transition may only be followed if the current char in the haystack falls in the inclusive range of chars specified.

• start : Nat

  The inclusive start of the char range.

• end : Nat

  The inclusive end of the char range.

• next : Fin n

  The identifier of the state to transition to.

instance NFA.Checked.instBEqTransition {n✝ : Nat} : BEq (Transition n✝)

Equations

• NFA.Checked.instBEqTransition = { beq := NFA.Checked.beqTransition✝ }

instance NFA.Checked.instDecidableEqTransition {n✝ : Nat} : DecidableEq (Transition n✝)

Equations

• NFA.Checked.instDecidableEqTransition = NFA.Checked.decEqTransition✝

def NFA.Checked.Transition.matches {n : Nat} (trans : Transition n) (c : Char) : Bool

check if c falls in the inclusive range of chars specified in Transition trans

Equations

• trans.matches c = (decide (trans.start ≤ ↑c.val.toFin) && decide (↑c.val.toFin ≤ trans.end))

inductive NFA.Checked.State (n : Nat) : Type

A state in an NFA, the elements of Fin n refer to existing states in the NFA.

• Empty {n : Nat} (next : Fin n) : State n

  An empty state whose only purpose is to forward the automaton to another state via an unconditional epsilon transition.

• NextChar {n : Nat} (offset : Nat) (next : Fin n) : State n

  use netx char

• Fail {n : Nat} : State n

  Fail, force backtracking

• Eat {n : Nat} (mode : EatMode n) (next : Fin n) : State n

  remove Frame.Step in stack

• ChangeFrameStep {n : Nat} (fr to : Fin n) : State n

  change Frame.Step in stack and force backtracking

• RemoveFrameStep {n : Nat} (sid : Fin n) : State n

  remove Frame.Step in stack and force backtrack

• BackRef {n : Nat} (b : Nat) (case_insensitive : Bool) (sid : Fin n) : State n

  A state with a single transition may only be followed if the current chars match the backrefence to the capturung group.

• ByteRange {n : Nat} (trans : Transition n) : State n

  A state with a single transition that can only be taken if the current input symbol is in a particular range of chars.

• SparseTransitions {n : Nat} (transitions : Array (Transition n)) : State n

  A sequence of transitions used to represent a sparse state.

• Look {n : Nat} (look : NFA.Look) (next : Fin n) : State n

  A conditional epsilon transition satisfied via some sort of look-around.

• Union {n : Nat} (alternates : Array (Fin n)) : State n

  An alternation such that there exists an epsilon transition to all states in alternates, where matches found via earlier transitions are preferred over later transitions.

• UnionReverse {n : Nat} (alternates : Array (Fin n)) : State n

  An alternation such that there exists an epsilon transition to all states in alternates, where matches found via later transitions are preferred over earlier transitions.

• BinaryUnion {n : Nat} (alt1 alt2 : Fin n) : State n

  An alternation such that there exists precisely two unconditional epsilon transitions

• Capture {n : Nat} (role : Capture.Role) (next : Fin n) (pattern_id : PatternID) (group slot : Nat) (isValid : Capture.IsValid role group slot) : State n

  An empty state that records a capture location. slot in this context refers to the specific capture group slot offset that is being recorded. Each capturing group has two slots corresponding to the start and end of the matching portion of that group.

• Match {n : Nat} (pattern_id : PatternID) : State n

  A match state. There is at least one such occurrence of this state for each regex that can match that is in this NFA.

instance NFA.Checked.instBEqState {n✝ : Nat} : BEq (State n✝)

Equations

• NFA.Checked.instBEqState = { beq := NFA.Checked.beqState✝ }

instance NFA.Checked.instDecidableEqState {n✝ : Nat} : DecidableEq (State n✝)

Equations

• NFA.Checked.instDecidableEqState = NFA.Checked.decEqState✝

instance NFA.Checked.instBEqState_1 {n : Nat} : BEq (State n)

Equations

• NFA.Checked.instBEqState_1 = { beq := NFA.Checked.beq'✝ }

def NFA.Checked.State.toString {n : Nat} : State n → String

Equations

• One or more equations did not get rendered due to their size.
• (NFA.Checked.State.Empty next).toString = toString "State.Empty => " ++ toString next ++ toString ""
• (NFA.Checked.State.NextChar offset next).toString = toString "State.NextChar offset " ++ toString offset ++ toString " => " ++ toString next ++ toString ""
• NFA.Checked.State.Fail.toString = toString "State.Fail"
• (NFA.Checked.State.Eat s next).toString = toString "State.Eat " ++ toString s ++ toString " => " ++ toString next ++ toString ""
• (NFA.Checked.State.ChangeFrameStep f t).toString = toString "State.ChangeFrameStep from " ++ toString f ++ toString " to " ++ toString t ++ toString ""
• (NFA.Checked.State.RemoveFrameStep sid).toString = toString "State.RemoveFrameStep " ++ toString sid ++ toString ""
• (NFA.Checked.State.Look look next).toString = toString "State.Look " ++ toString look ++ toString " => " ++ toString next ++ toString ""
• (NFA.Checked.State.BinaryUnion alt1 alt2).toString = toString "State.BinaryUnion (" ++ toString alt1 ++ toString ", " ++ toString alt2 ++ toString ")"
• (NFA.Checked.State.Match pattern_id).toString = toString "State.Match (" ++ toString pattern_id ++ toString ")"

instance NFA.Checked.instToStringState {n : Nat} : ToString (State n)

Equations

• NFA.Checked.instToStringState = { toString := fun (s : NFA.Checked.State n) => s.toString }

structure NFA.Checked.NFA : Type

A char oriented Thompson non-deterministic finite automaton (NFA) with n states

• n : Nat

  number of states

• states : Array (State self.n)

  states of the NFA

• groups : Array Nat

  capture groups which may match with a empty string

• slots : Array Capture.SlotGroup

  Array of (slot, group) pairs of captures

• unanchored_prefix_in_backtrack : Bool

  simulate a unanchored prefix by the backtracker

• isEq : self.n = self.states.size

  assertion that n equals size of states

• slotsValid : Slots.Valid self.slots

  slots are valid

instance NFA.Checked.instInhabitedNFA : Inhabited NFA

Equations

• One or more equations did not get rendered due to their size.

instance NFA.Checked.instCoeFinNSizeStateStates {nfa : NFA} : Coe (Fin nfa.n) (Fin nfa.states.size)

Equations

• NFA.Checked.instCoeFinNSizeStateStates = { coe := fun (n : Fin nfa.n) => Fin.castLE ⋯ n }

def NFA.Checked.toString (nfa : NFA) : String

Equations

• One or more equations did not get rendered due to their size.

instance NFA.Checked.instToStringNFA : ToString NFA

Equations

• NFA.Checked.instToStringNFA = { toString := NFA.Checked.toString }

def NFA.toCkeckedState (s : Unchecked.State) (n : Nat) (h : s.nextOf < n) : Checked.State n

Equations

• One or more equations did not get rendered due to their size.
• NFA.toCkeckedState (NFA.Unchecked.State.Empty next) n h_2 = NFA.Checked.State.Empty ⟨next, h_2⟩
• NFA.toCkeckedState (NFA.Unchecked.State.NextChar offset next) n h_2 = NFA.Checked.State.NextChar offset ⟨next, h_2⟩
• NFA.toCkeckedState NFA.Unchecked.State.Fail n h_2 = NFA.Checked.State.Fail
• NFA.toCkeckedState (NFA.Unchecked.State.Eat (NFA.Unchecked.EatMode.Until s_2) next) n h_2 = NFA.Checked.State.Eat (NFA.Checked.EatMode.Until ⟨s_2, ⋯⟩) ⟨next, ⋯⟩
• NFA.toCkeckedState (NFA.Unchecked.State.Eat (NFA.Unchecked.EatMode.ToLast s_2) next) n h_2 = NFA.Checked.State.Eat (NFA.Checked.EatMode.ToLast ⟨s_2, ⋯⟩) ⟨next, ⋯⟩
• NFA.toCkeckedState (NFA.Unchecked.State.ChangeFrameStep f t) n h_2 = NFA.Checked.State.ChangeFrameStep ⟨f, ⋯⟩ ⟨t, ⋯⟩
• NFA.toCkeckedState (NFA.Unchecked.State.RemoveFrameStep t) n h_2 = NFA.Checked.State.RemoveFrameStep ⟨t, h_2⟩
• NFA.toCkeckedState (NFA.Unchecked.State.BackRef b f sid) n h_2 = NFA.Checked.State.BackRef b f ⟨sid, h_2⟩
• NFA.toCkeckedState (NFA.Unchecked.State.Look look next) n h_2 = NFA.Checked.State.Look look ⟨next, h_2⟩
• NFA.toCkeckedState (NFA.Unchecked.State.Capture role next pattern_id group slot isValid) n h_2 = NFA.Checked.State.Capture role ⟨next, h_2⟩ pattern_id group slot isValid
• NFA.toCkeckedState (NFA.Unchecked.State.BinaryUnion alt1 alt2) n h_2 = NFA.Checked.State.BinaryUnion ⟨alt1, ⋯⟩ ⟨alt2, ⋯⟩
• NFA.toCkeckedState (NFA.Unchecked.State.Match pattern_id) n h_2 = NFA.Checked.State.Match pattern_id

def NFA.toFun (states : Array Unchecked.State) (h : ∀ (i : Nat) (x : i < states.size), states[i].nextOf < states.size) : { x : Unchecked.State // x ∈ states } → Checked.State states.size

Equations

• NFA.toFun states h = fun (s : { x : NFA.Unchecked.State // x ∈ states }) => NFA.toCkeckedState s.val states.size ⋯