From 9fa9055007f28f3e90a3a44024dbf2ba9ff6ea8b Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Mon, 2 Sep 2024 17:46:04 +0100
Subject: Define a type of well-kinded types.

---
 src/Inky/Type.idr | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

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

diff --git a/src/Inky/Type.idr b/src/Inky/Type.idr
index 8c4285e..096518a 100644
--- a/src/Inky/Type.idr
+++ b/src/Inky/Type.idr
@@ -1,7 +1,7 @@
 module Inky.Type
 
 import Data.Bool.Decidable
-import Data.DPair
+import public Data.DPair
 import Inky.Binding
 import Inky.Env
 import Inky.Kind
@@ -108,3 +108,7 @@ checkKindPrf env k (TEmbed a) with (synthKindPrf env a) | (synthKind env a)
     _ | RTrue eq | _ = RTrue (TEmbed aKind eq)
     _ | RFalse neq | _ = RFalse (\case TEmbed aKind' eq => neq $ trans eq $ synthKindUniq aKind' aKind)
   _ | No aUnkind | _ = RFalse (\case TEmbed aKind Refl => aUnkind _ aKind)
+
+public export
+ATy : {w : World} -> Env Kind w -> Type
+ATy env = Subset (RawCTy w) (CheckKind env KStar)
-- 
cgit v1.2.3