diff options
Diffstat (limited to 'src/Obs/Syntax.idr')
| -rw-r--r-- | src/Obs/Syntax.idr | 7 |
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" |