TyRE.Parser.GroupThompson

Definitions

record NextStates : Type

Totality: total
Visibility: public export
Constructor: 

MkNextStates : CharCond -> List (Maybe Nat) -> NextStates

Projections:

.condition : NextStates -> CharCond

.isSat : NextStates -> List (Maybe Nat)

.condition : NextStates -> CharCond

Totality: total
Visibility: public export

condition : NextStates -> CharCond

Totality: total
Visibility: public export

.isSat : NextStates -> List (Maybe Nat)

Totality: total
Visibility: public export

isSat : NextStates -> List (Maybe Nat)

Totality: total
Visibility: public export

record GroupSM : Type

Totality: total
Visibility: public export
Constructor: 

MkGroupSM : List (Maybe Nat) -> List (Nat, NextStates) -> Nat -> GroupSM

Projections:

.initStates : GroupSM -> List (Maybe Nat)

.max : GroupSM -> Nat

.statesWithNext : GroupSM -> List (Nat, NextStates)

.initStates : GroupSM -> List (Maybe Nat)

Totality: total
Visibility: public export

initStates : GroupSM -> List (Maybe Nat)

Totality: total
Visibility: public export

.statesWithNext : GroupSM -> List (Nat, NextStates)

Totality: total
Visibility: public export

statesWithNext : GroupSM -> List (Nat, NextStates)

Totality: total
Visibility: public export

.max : GroupSM -> Nat

Totality: total
Visibility: public export

max : GroupSM -> Nat

Totality: total
Visibility: public export

groupSM : TyRE a -> GroupSM

Totality: total
Visibility: public export