nominalterms.hs

  newtype TermFormerID = TermFormerID Natural deriving (Eq, Show)
  -- Used for dynamic sequences of name usage. For example, memory locations in an imperitive program. Models binding arities.
  data BindingToken a = Create Name
                 | Destroy Name
                 | RawTerm a
                 | Constant a deriving (Eq, Show, Functor, Foldable, Traversable)


  data NominalTerm a = Atom Name
                   | Variable Permutation Name
                   | BindingSequence [BindingToken a]
                   | TermFormer TermFormerID [NominalTerm a] deriving (Eq, Show, Functor,  Foldable, Traversable)


  makeClassy ''BindingToken
  makeClassyPrisms ''BindingToken
  makeClassy ''NominalTerm
  makeClassyPrisms ''NominalTerm