From f19665eac65f9a37dcde85eb58e7d4b5b4a22bcf Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 1 Apr 2023 13:58:46 +0100
Subject: Make environments do weakening lazily.

This is in anticipation for defining well-formed thinnings.
---
 src/Core/Declarative.idr | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/Core/Declarative.idr')

diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr
index 8efda89..4a27923 100644
--- a/src/Core/Declarative.idr
+++ b/src/Core/Declarative.idr
@@ -27,9 +27,9 @@ data EnvWf where
     EnvWf [<]
   (:<) :
     EnvWf env ->
-    TypeWf env a ->
+    TypeWf env (wkn a thin) ->
     ---
-    EnvWf (env :< a)
+    EnvWf (Add env thin a)
 
 data TypeWf where
   SetType :
-- 
cgit v1.2.3