From a8d4301d0d6e62b75abecb8e00e26e14c890a42d Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Sat, 17 Dec 2022 17:37:11 +0000
Subject: Make fullBounds public.

---
 src/Obs/Term.idr | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src/Obs/Term.idr')

diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index cb9701de..3e2d4b7 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -29,6 +29,7 @@ data Block : Nat -> Type where
 
 -- Operations ------------------------------------------------------------------
 
+export
 fullBounds : Term n -> Bounds
 fullBounds (Var x i)  = x
 fullBounds (Sort x s) = x
-- 
cgit v1.2.3