NCILL.Types

module NCILL.Types where

open import Data.Nat

-- TYPES
------------------------------------------------------------------------

data Ty : Set where
  κ    : ℕ → Ty
  _⊸_  : Ty → Ty → Ty
  _⊸ʳ_ : Ty → Ty → Ty -- either reversed, or argument on the right.
  _⊗_  : Ty → Ty → Ty
  _⊕_  : Ty → Ty → Ty
  _&_  : Ty → Ty → Ty
  ♯1   : Ty
  ♯0   : Ty
  ♯⊤   : Ty

infixr 8  _⊸_
infixr 8  _⊸ʳ_
infixr 9  _⊕_
infixr 10 _&_
infixr 11 _⊗_