Add sum types.

1 files changed, 17 insertions, 0 deletions

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index b8fca7b..03367dc 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -51,6 +51,23 @@ abstractSyntax ctx (Fst t) = do
 abstractSyntax ctx (Snd t) = do
   t <- abstractSyntaxBounds ctx t
   pure (Snd t)
+abstractSyntax ctx (Sum a b) = do
+  a <- abstractSyntaxBounds ctx a
+  b <- abstractSyntaxBounds ctx b
+  pure (Sum a b)
+abstractSyntax ctx (Left t) = do
+  t <- abstractSyntaxBounds ctx t
+  pure (Left t)
+abstractSyntax ctx (Right t) = do
+  t <- abstractSyntaxBounds ctx t
+  pure (Right t)
+abstractSyntax ctx (Case t s b f g) = do
+  t <- abstractSyntaxBounds ctx t
+  s <- abstractSyntaxBounds ctx s
+  b <- abstractSyntaxBounds ctx b
+  f <- abstractSyntaxBounds ctx f
+  g <- abstractSyntaxBounds ctx g
+  pure (Case t s b f g)
 abstractSyntax ctx Top = pure Top
 abstractSyntax ctx Point = pure Point
 abstractSyntax ctx Bottom = pure Bottom