From 37acb2efba1cd159bda5d163192e2aba70c4e26b Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Fri, 22 Dec 2023 23:19:20 +0100
Subject: Stuff

---
 src/AST.hs | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'src/AST.hs')

diff --git a/src/AST.hs b/src/AST.hs
index 42967bc..ba018f5 100644
--- a/src/AST.hs
+++ b/src/AST.hs
@@ -22,6 +22,8 @@ data Term
   | TIMax Term Term      -- ^ Maximum of two levels
   | TISucc Term          -- ^ Level + 1
 
+  | TAnnot (OfType Term Term)  -- ^ term : type
+
   -- Temporary stuff until we have proper inductive types:
   | TOne                   -- ^ The unit type
   | TUnit                  -- ^ The element of the unit type
@@ -31,4 +33,11 @@ data Term
   | TProj2 Term            -- ^ Second projection of a dependent pair
   deriving (Show)
 
+data Definition = Definition Name (OfType Term Term)
+  deriving (Show)
+
 type Env = Map Name Term
+
+data OfType a b = a :| b
+  deriving (Show)
+infix 1 :|
-- 
cgit v1.2.3-70-g09d2