blob: 603d8a93136c5eb154d3575aeebed601665244ef (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
module Core.Term
import Core.Context
import Core.Var
%prefix_record_projections off
-- 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
|
