blob: d1aafc43b36df9147861b295f69793fd626de0cd (
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
26
27
28
29
30
31
32
33
34
35
36
37
|
module CBPV.Context where
open import Data.Bool using (Bool)
open import Data.String using (String)
import Data.String.Properties as String
open import Relation.Binary.Definitions using (DecidableEquality)
open import CBPV.Type
abstract
Name : Set
Name = String
𝔪 : Name
𝔪 = "𝔪"
record Named : Set where
constructor _:-_
field
name : Name
ofType : ValType
open Named public
infixl 5 _:<_ _++_
data Context : Set where
[<] : Context
_:<_ : Context → (ex : Named) → Context
pattern [<_:-_] x A = [<] :< (x :- A)
pattern [<_:-_,_:-_] x A y A′ = [<] :< (x :- A) :< (y :- A′)
_++_ : Context → Context → Context
Γ ++ [<] = Γ
Γ ++ (Δ :< ex) = Γ ++ Δ :< ex
|
