module CBPV.Type where

open import Data.List

infixr 5 _⟶_ _⟶⋆_ _⟶′⋆_

data ValType : Set
data CompType : Set

data ValType where
  U   : CompType → ValType
  𝟙   : ValType
  _×_ : ValType → ValType → ValType
  _+_ : ValType → ValType → ValType

data CompType where
  F   : ValType → CompType
  _×_ : CompType → CompType → CompType
  _⟶_ : ValType → CompType → CompType

_⟶⋆_ : List ValType → CompType → CompType
Γ ⟶⋆ B = foldr _⟶_ B Γ

_⟶′⋆_ : List CompType → CompType → CompType
Γ ⟶′⋆ B = foldr (λ ◌ᵃ ◌ᵇ → U ◌ᵃ ⟶ ◌ᵇ) B Γ