blob: 2b52f545fbde07b7603afbac0ba0fad90a351ccd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
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 Γ
|
