------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- The syntax of types with the Nehemiah plugin.
------------------------------------------------------------------------

module Nehemiah.Syntax.Type where

import Parametric.Syntax.Type as Type

data Base : Type.Structure where
  base-int : Base
  base-bag : Base

open Type.Structure Base public

pattern int = base base-int
pattern bag = base base-bag