Stuff

1 files changed, 9 insertions, 0 deletions

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 :|