Add the True type.

1 files changed, 9 insertions, 2 deletions

diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index 71d070f..da2f9e4 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -11,9 +11,12 @@ import Text.PrettyPrint.Prettyprinter
 
 public export
 data Syntax : Type where
-  Var  : Bounds -> String -> Syntax
+  Var   : Bounds -> String -> Syntax
   -- Sorts
-  Sort : Bounds -> Sort -> Syntax
+  Sort  : Bounds -> Sort -> Syntax
+  -- True
+  Top   : Bounds -> Syntax
+  Point : Bounds -> Syntax
 
 public export
 record Definition where
@@ -28,6 +31,8 @@ record Definition where
 fullBounds : Syntax -> Bounds
 fullBounds (Var x str) = x
 fullBounds (Sort x s)  = x
+fullBounds (Top x)     = x
+fullBounds (Point x)   = x
 
 -- Pretty Print ----------------------------------------------------------------
 
@@ -35,6 +40,8 @@ export
 Pretty Syntax where
   prettyPrec d (Var x str) = pretty str
   prettyPrec d (Sort x s)  = prettyPrec d s
+  prettyPrec d (Top x)     = pretty "()"
+  prettyPrec d (Point x)   = pretty "_"
 
 export
 Pretty Definition where