summaryrefslogtreecommitdiff
path: root/src/Obs/Abstract.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Obs/Abstract.idr')
-rw-r--r--src/Obs/Abstract.idr2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index bac6d04..fe00621 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -38,6 +38,8 @@ abstractSyntax ctx (Var b str) = do
| Nothing => report b "unbound variable: \{str}"
pure (Var b i)
abstractSyntax ctx (Sort b s) = pure (Sort b s)
+abstractSyntax ctx (Top b) = pure (Top b)
+abstractSyntax ctx (Point b) = pure (Point b)
export
abstractDefinition : Context n -> Definition -> Error (Definition n)