From 97f4dfe968f55e115f61ef43c37b8e7a16b6c3fd Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Sun, 18 Dec 2022 12:04:27 +0000
Subject: Remove fullBounds from Syntax.

---
 src/Obs/Syntax.idr | 8 --------
 1 file changed, 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
-- 
cgit v1.2.3