Add False type.

1 files changed, 15 insertions, 7 deletions

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