diff options
Diffstat (limited to 'src/Obs/Term.idr')
| -rw-r--r-- | src/Obs/Term.idr | 7 |
1 files changed, 7 insertions, 0 deletions
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" |