blob: 930e68f354f81d29b811ddbd5475145405dc77e2 (
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 Core.Term
import Core.Context
import Core.Var
import Core.Thinning
-- Definition ------------------------------------------------------------------
public export
data Term : Context -> Type where
Var : Var sx -> Term sx
Set : Term sx
Pi : (n : Name) -> Term sx -> Term (sx :< n) -> Term sx
Abs : (n : Name) -> Term (sx :< n) -> Term sx
App : Term sx -> Term sx -> Term sx
%name Term t, u, v
-- Operations ------------------------------------------------------------------
public export
wkn : Term sx -> sx `Thins` sy -> Term sy
wkn (Var i) thin = Var $ wkn i thin
wkn Set thin = Set
wkn (Pi n t u) thin = Pi n (wkn t thin) (wkn u $ keep thin n)
wkn (Abs n t) thin = Abs n (wkn t $ keep thin n)
wkn (App t u) thin = App (wkn t thin) (wkn u thin)
|
