module regex where

open import Level renaming ( suc to succ ; zero to Zero )
open import Data.Fin
open import Data.List 
open import Data.Bool using ( Bool ; true ; false )
open import  Relation.Binary.PropositionalEquality

data Regex   ( Σ : Set  ) : Set  where
   _*    : Regex  Σ → Regex  Σ
   _&_   : Regex  Σ → Regex  Σ → Regex Σ
   <_>  : List   Σ → Regex  Σ


-- data  In2   : Set  where
--    a : In2
--    b : In2

open import automaton

regex2nfa :  Regex In2 → NAutomaton ? In2 ? ? ? ?
regex2nfa = ?