diff options
| -rw-r--r-- | src/Core/Term.idr | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/src/Core/Term.idr b/src/Core/Term.idr new file mode 100644 index 0000000..603d8a9 --- /dev/null +++ b/src/Core/Term.idr @@ -0,0 +1,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 |