Add False type.

1 files changed, 8 insertions, 3 deletions

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index fe00621..1b72965 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -37,9 +37,14 @@ abstractSyntax ctx (Var b str) = do
   let Just i = lookup str ctx
     | 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)
+abstractSyntax ctx (Sort b s) = pure (Sort b s)
+abstractSyntax ctx (Top b) = pure (Top b)
+abstractSyntax ctx (Point b) = pure (Point b)
+abstractSyntax ctx (Bottom b) = pure (Bottom b)
+abstractSyntax ctx (Absurd b a t) = do
+  a <- abstractSyntax ctx a
+  t <- abstractSyntax ctx t
+  pure (Absurd b a t)
 
 export
 abstractDefinition : Context n -> Definition -> Error (Definition n)