Add Container types.

1 files changed, 24 insertions, 0 deletions

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index 03367dc..48709c1 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -68,6 +68,30 @@ abstractSyntax ctx (Case t s b f g) = do
   f <- abstractSyntaxBounds ctx f
   g <- abstractSyntaxBounds ctx g
   pure (Case t s b f g)
+abstractSyntax ctx (Container a s s') = do
+  a <- abstractSyntaxBounds ctx a
+  s <- abstractSyntaxBounds ctx s
+  s' <- abstractSyntaxBounds ctx s'
+  pure (Container a s s')
+abstractSyntax ctx (MkContainer t p f) = do
+  t <- abstractSyntaxBounds ctx t
+  p <- abstractSyntaxBounds ctx p
+  f <- abstractSyntaxBounds ctx f
+  pure (MkContainer t p f)
+abstractSyntax ctx (Tag t) = do
+  t <- abstractSyntaxBounds ctx t
+  pure (Tag t)
+abstractSyntax ctx (Position t) = do
+  t <- abstractSyntaxBounds ctx t
+  pure (Position t)
+abstractSyntax ctx (Next t) = do
+  t <- abstractSyntaxBounds ctx t
+  pure (Next t)
+abstractSyntax ctx (Sem s a t) = do
+  s <- abstractSyntaxBounds ctx s
+  a <- abstractSyntaxBounds ctx a
+  t <- abstractSyntaxBounds ctx t
+  pure (Sem s a t)
 abstractSyntax ctx Top = pure Top
 abstractSyntax ctx Point = pure Point
 abstractSyntax ctx Bottom = pure Bottom