blob: 1b050caf0cdc75291ebea9441df25b00e2012a20 (
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.Thinning
import public Data.Fin
-- Definition ------------------------------------------------------------------
public export
data Term : Nat -> Type where
Var : Fin n -> Term n
Set : Term n
Pi : Term n -> Term (S n) -> Term n
Abs : Term (S n) -> Term n
App : Term n -> Term n -> Term n
%name Term t, u, v
-- Weakening -------------------------------------------------------------------
public export
wkn : Term m -> m `Thins` n -> Term n
wkn (Var i) thin = Var (wkn i thin)
wkn Set thin = Set
wkn (Pi t u) thin = Pi (wkn t thin) (wkn u $ keep thin)
wkn (Abs t) thin = Abs (wkn t $ keep thin)
wkn (App t u) thin = App (wkn t thin) (wkn u thin)
|
