summaryrefslogtreecommitdiff
path: root/src/Obs/Syntax.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Obs/Syntax.idr')
-rw-r--r--src/Obs/Syntax.idr8
1 files changed, 0 insertions, 8 deletions
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index da2f9e4..056c86a 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -26,14 +26,6 @@ record Definition where
ty : Syntax
tm : Syntax
--- Operations ------------------------------------------------------------------
-
-fullBounds : Syntax -> Bounds
-fullBounds (Var x str) = x
-fullBounds (Sort x s) = x
-fullBounds (Top x) = x
-fullBounds (Point x) = x
-
-- Pretty Print ----------------------------------------------------------------
export