summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Inky/Type.idr4
1 files changed, 2 insertions, 2 deletions
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