Add the True type.

1 files changed, 9 insertions, 2 deletions

diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index d5213d2..2cc2f93 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -12,9 +12,12 @@ import Text.PrettyPrint.Prettyprinter
 
 public export
 data Term : Nat -> Type where
-  Var  : Bounds -> Fin n -> Term n
+  Var   : Bounds -> Fin n -> Term n
   -- Sorts
-  Sort : Bounds -> Sort -> Term n
+  Sort  : Bounds -> Sort -> Term n
+  -- True
+  Top   : Bounds -> Term n
+  Point : Bounds -> Term n
 
 public export
 record Definition (n : Nat) where
@@ -35,6 +38,8 @@ export
 fullBounds : Term n -> Bounds
 fullBounds (Var x i)  = x
 fullBounds (Sort x s) = x
+fullBounds (Top x)     = x
+fullBounds (Point x)   = x
 
 -- Pretty Print ----------------------------------------------------------------
 
@@ -42,6 +47,8 @@ export
 Pretty (Term n) where
   prettyPrec d (Var x i)  = pretty "$\{show i}"
   prettyPrec d (Sort x s) = prettyPrec d s
+  prettyPrec d (Top x)    = pretty "()"
+  prettyPrec d (Point x)  = pretty "_"
 
 export
 Pretty (Definition n) where