blob: 7fea482a910f14c286457ddee2e10885a18ee6e6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
module Core.Term
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
|
