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/Abstract.idr | 2 ++
 1 file changed, 2 insertions(+)

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

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index bac6d04..fe00621 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -38,6 +38,8 @@ abstractSyntax ctx (Var b str) = do
     | Nothing => report b "unbound variable: \{str}"
   pure (Var b i)
 abstractSyntax ctx (Sort b s)  = pure (Sort b s)
+abstractSyntax ctx (Top b)     = pure (Top b)
+abstractSyntax ctx (Point b)   = pure (Point b)
 
 export
 abstractDefinition : Context n -> Definition -> Error (Definition n)
-- 
cgit v1.2.3