From b6fb551360b283c38b3ede9ef3e6d2922bd62b58 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Sun, 18 Dec 2022 12:00:01 +0000
Subject: Add the True type.

---
 src/Obs/Term.idr | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

(limited to 'src/Obs/Term.idr')

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
-- 
cgit v1.2.3