From 9af1a41a58575508c8d2dff6e7b25a5caac8aadc Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Sun, 8 Jan 2023 00:56:11 +0000
Subject: Add box types.

---
 src/Obs/Abstract.idr | 9 +++++++++
 1 file changed, 9 insertions(+)

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

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
-- 
cgit v1.2.3