Add box types.

1 files changed, 9 insertions, 0 deletions

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index 16b0c92..94b208c 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -98,6 +98,15 @@ abstractSyntax ctx (If {returnType, discriminant, true, false}) = do
   true <- abstractSyntaxBounds ctx true
   false <- abstractSyntaxBounds ctx false
   pure (If {returnType, discriminant, true, false})
+abstractSyntax ctx (Box {prop}) = do
+  prop <- abstractSyntaxBounds ctx prop
+  pure (Box {prop})
+abstractSyntax ctx (MkBox {arg}) = do
+  arg <- abstractSyntaxBounds ctx arg
+  pure (MkBox {arg})
+abstractSyntax ctx (Unbox {arg}) = do
+  arg <- abstractSyntaxBounds ctx arg
+  pure (Unbox {arg})
 abstractSyntax ctx Top = pure Top
 abstractSyntax ctx Point = pure Point
 abstractSyntax ctx Bottom = pure Bottom