1 files changed, 22 insertions, 0 deletions
diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index ef90cb8..9215dda 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -57,6 +57,28 @@ abstractSyntax ctx (Absurd bounds a t) = do
   a <- abstractSyntax ctx a
   t <- abstractSyntax ctx t
   pure (Absurd bounds a t)
+abstractSyntax ctx (Equal bounds t u) = do
+  t <- abstractSyntax ctx t
+  u <- abstractSyntax ctx u
+  pure (Equal bounds t u)
+abstractSyntax ctx (Refl bounds t) = do
+  t <- abstractSyntax ctx t
+  pure (Refl bounds t)
+abstractSyntax ctx (Transp bounds t b u t' e) = do
+  t <- abstractSyntax ctx t
+  b <- abstractSyntax ctx b
+  u <- abstractSyntax ctx u
+  t' <- abstractSyntax ctx t'
+  e <- abstractSyntax ctx e
+  pure (Transp bounds t b u t' e)
+abstractSyntax ctx (Cast bounds b e t) = do
+  b <- abstractSyntax ctx b
+  e <- abstractSyntax ctx e
+  t <- abstractSyntax ctx t
+  pure (Cast bounds b e t)
+abstractSyntax ctx (CastId bounds t) = do
+  t <- abstractSyntax ctx t
+  pure (CastId bounds t)
 
 abstractDefinition : Context n -> Definition -> Logging ann (Definition n)
 abstractDefinition ctx def = pure $ MkDefinition