diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-03-31 16:44:02 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-03-31 16:44:02 +0100 |
| commit | 77d68435806e5a4c1f9e8c30d69d8d033539c570 (patch) | |
| tree | b4afccbc649b4cc22d4017d60b07d1c3920653c5 /src/Core | |
| parent | 9df5dc217cb11d4c8d6af6d1deb35fd8f174b797 (diff) | |
Define Terms.
Diffstat (limited to 'src/Core')
| -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 |