Add box types.

1 files changed, 6 insertions, 0 deletions

diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index d325f1a..b290240 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -49,6 +49,8 @@ data Constructor : Unsorted.Family Relevance where
   Bool : Constructor ctx
   True : Constructor ctx
   False : Constructor ctx
+  Box : (prop : TypeNormalForm ctx) -> Constructor ctx
+  MkBox : Constructor ctx
   Top : Constructor ctx
   Bottom : Constructor ctx
 
@@ -139,6 +141,8 @@ prettyPrecCnstr d (Pair {indexRel, elementRel, prf, first, second}) =
 prettyPrecCnstr d Bool = pretty "Bool"
 prettyPrecCnstr d True = pretty "True"
 prettyPrecCnstr d False = pretty "False"
+prettyPrecCnstr d (Box {prop}) = prettyApp d (pretty "Box") [prettyPrec App prop]
+prettyPrecCnstr d MkBox = pretty "box"
 prettyPrecCnstr d Top = pretty "()"
 prettyPrecCnstr d Bottom = pretty "Void"
 
@@ -224,6 +228,8 @@ renameCnstr (Pair {indexRel, elementRel, prf, first, second}) f =
 renameCnstr Bool f = Bool
 renameCnstr True f = True
 renameCnstr False f = False
+renameCnstr (Box {prop}) f = Box {prop = rename prop f}
+renameCnstr MkBox f = MkBox
 renameCnstr Top f = Top
 renameCnstr Bottom f = Bottom