blob: ef657ae49b700dc7cb8b1ef134229b3cafac8c20 (
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
|
module SOAS.Context
infixr 4 :-
public export
record (.extension) (type : Type) where
constructor (:-)
0 name : String
ofType : type
public export
data (.Ctx) : (type : Type) -> Type where
Lin : type.Ctx
(:<) : (ctx : type.Ctx) -> (namety : type.extension) -> type.Ctx
public export
data (.Erased) : type.Ctx -> Type where
Z : [<].Erased
S : ctx.Erased -> (ctx :< x).Erased
public export
(.toNat) : ctx.Erased -> Nat
(Z).toNat = 0
(S length).toNat = S length.toNat
public export
(++) : (ctx1,ctx2 : type.Ctx) -> type.Ctx
ctx1 ++ [<] = ctx1
ctx1 ++ (ctx2 :< ty) = (ctx1 ++ ctx2) :< ty
|
