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/Term.idr | 7 +++++++
 1 file changed, 7 insertions(+)

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

diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index 8829038..8f03b5d 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -62,6 +62,10 @@ data Term : Nat -> Type where
   If : (returnType : LambdaForm n) ->
     (discriminant, true, false : WithBounds (Term n)) ->
     Term n
+  -- Box Types
+  Box : (prop : WithBounds (Term n)) -> Term n
+  MkBox : (arg : WithBounds (Term n)) -> Term n
+  Unbox : (arg : WithBounds (Term n)) -> Term n
   -- True
   Top : Term n
   Point : Term n
@@ -145,6 +149,9 @@ prettyPrec d (If {returnType, discriminant, true, false}) =
   , prettyPrecBounds App true
   , prettyPrecBounds App false
   ]
+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 Top = pretty "()"
 prettyPrec d Point = pretty "tt"
 prettyPrec d Bottom = pretty "Void"
-- 
cgit v1.2.3