Add box types.

1 files changed, 7 insertions, 0 deletions

diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index ea7772e..bab23ac 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -52,6 +52,10 @@ data Syntax : Type where
   True : Syntax
   False : Syntax
   If : (returnType : LambdaForm) -> (discriminant, true, false : WithBounds Syntax) -> Syntax
+  -- Box Types
+  Box : (prop : WithBounds Syntax) -> Syntax
+  MkBox : (arg : WithBounds Syntax) -> Syntax
+  Unbox : (arg : WithBounds Syntax) -> Syntax
   -- True
   Top : Syntax
   Point : Syntax
@@ -119,6 +123,9 @@ prettyPrec d (Position {arg}) = prettyApp d (pretty "Position") [prettyPrecBound
 prettyPrec d (Next {arg}) = prettyApp d (pretty "nextIndex") [prettyPrecBounds App arg]
 prettyPrec d (Sem {pred, arg}) =
   prettyApp d (pretty "extension") [prettyPrecLambda App pred, prettyPrecBounds App arg]
+prettyPrec d (Box {prop}) = prettyApp d (pretty "Box") [prettyPrecBounds App prop]
+prettyPrec d (MkBox {arg}) = prettyApp d (pretty "box") [prettyPrecBounds App arg]
+prettyPrec d (Unbox {arg}) = prettyApp d (pretty "unbox") [prettyPrecBounds App arg]
 prettyPrec d Bool = pretty "Bool"
 prettyPrec d True = pretty "True"
 prettyPrec d False = pretty "False"