diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2023-01-08 00:56:11 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2023-01-08 00:56:11 +0000 |
| commit | 9af1a41a58575508c8d2dff6e7b25a5caac8aadc (patch) | |
| tree | 51522621c0726b19216e13cb18ddc19483c48b54 /src/Obs/Term.idr | |
| parent | 028685cef60b5d32e42a0951856e78f39165635a (diff) | |
Add box types.
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" |