From 3896701f162a5b6fb2923ebe3fee5066f74f2b5c Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 1 Apr 2023 14:02:00 +0100
Subject: Define well-formed thinnings.

---
 src/Core/Declarative.idr | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

(limited to 'src/Core')

diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr
index 4a27923..319b465 100644
--- a/src/Core/Declarative.idr
+++ b/src/Core/Declarative.idr
@@ -141,12 +141,23 @@ data TermConv where
     ---
     TermConv env (App t a) (App u b) (subst g $ sub1 a)
 
-%name EnvWf wf
+%name EnvWf envWf
 %name TypeWf wf
 %name TypeConv conv
 %name TermWf wf
 %name TermConv conv
 
+public export
+data ThinWf : sx `Thins` sy -> Env sy -> Env sx -> Type where
+  IdWf : ThinWf (id sx) env env
+  DropWf : ThinWf thin env2 env1 -> ThinWf (drop thin n) (Add env2 thin' a) env1
+  KeepWf :
+    ThinWf thin env2 env1 ->
+    {auto 0 prf : IsNotId thin} ->
+    ThinWf (keep thin n) (Add env2 (thin . thin') a) (Add env1 thin' a)
+
+%name ThinWf thinWf
+
 -- Well Formed Environment -----------------------------------------------------
 
 typeWfImpliesEnvWf : TypeWf env a -> EnvWf env
-- 
cgit v1.2.3