From 88b6df5dd91c062a96e646e6e6b0ac5fd57b7c03 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Sun, 18 Dec 2022 13:19:06 +0000
Subject: Add False type.

---
 src/Obs/Syntax.idr | 22 +++++++++++++++-------
 1 file changed, 15 insertions(+), 7 deletions(-)

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

diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index 056c86a..07c625b 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -11,12 +11,15 @@ 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
+  Top    : Bounds -> Syntax
+  Point  : Bounds -> Syntax
+  -- False
+  Bottom : Bounds -> Syntax
+  Absurd : Bounds -> Syntax -> Syntax -> Syntax
 
 public export
 record Definition where
@@ -31,9 +34,14 @@ record Definition where
 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 "_"
+  prettyPrec d (Sort x s) = prettyPrec d s
+  prettyPrec d (Top x) = pretty "()"
+  prettyPrec d (Point x) = pretty "_"
+  prettyPrec d (Bottom x) = pretty "Void"
+  prettyPrec d (Absurd x a t) =
+    parenthesise (d > Open) $
+    group $
+    fillSep [pretty "absurd", prettyPrec App a, prettyPrec App t]
 
 export
 Pretty Definition where
-- 
cgit v1.2.3