From 1d4f1054eec4eff215dae94566698da95beacf2e Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Mon, 2 Sep 2024 17:47:09 +0100
Subject: Remove unnecessary `where`.

---
 src/Inky/Type.idr | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/Inky/Type.idr')

diff --git a/src/Inky/Type.idr b/src/Inky/Type.idr
index 096518a..b8f95af 100644
--- a/src/Inky/Type.idr
+++ b/src/Inky/Type.idr
@@ -9,10 +9,10 @@ import Inky.OnlyWhen
 
 namespace Raw
   public export
-  data RawSTy : World -> Type where
+  data RawSTy : World -> Type
 
   public export
-  data RawCTy : World -> Type where
+  data RawCTy : World -> Type
 
   data RawSTy where
     TVar : (x : Name w) -> RawSTy w
-- 
cgit v1.2.3