diff options
Diffstat (limited to 'src/Obs/Abstract.idr')
| -rw-r--r-- | src/Obs/Abstract.idr | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr index 16b0c92..94b208c 100644 --- a/src/Obs/Abstract.idr +++ b/src/Obs/Abstract.idr @@ -98,6 +98,15 @@ abstractSyntax ctx (If {returnType, discriminant, true, false}) = do true <- abstractSyntaxBounds ctx true false <- abstractSyntaxBounds ctx false pure (If {returnType, discriminant, true, false}) +abstractSyntax ctx (Box {prop}) = do + prop <- abstractSyntaxBounds ctx prop + pure (Box {prop}) +abstractSyntax ctx (MkBox {arg}) = do + arg <- abstractSyntaxBounds ctx arg + pure (MkBox {arg}) +abstractSyntax ctx (Unbox {arg}) = do + arg <- abstractSyntaxBounds ctx arg + pure (Unbox {arg}) abstractSyntax ctx Top = pure Top abstractSyntax ctx Point = pure Point abstractSyntax ctx Bottom = pure Bottom |