From 0cce62f5e290d059b1545006c11b33d4329f00a3 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 1 Apr 2023 13:19:46 +0100
Subject: State properties of typing and reduction.

There correspond to lemmata 2.1--2.5 in Abel et. al.
---
 src/Core/Declarative.idr | 7 +++++++
 1 file changed, 7 insertions(+)

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

diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr
index 2561797..99cc1ab 100644
--- a/src/Core/Declarative.idr
+++ b/src/Core/Declarative.idr
@@ -146,3 +146,10 @@ data TermConv where
 %name TypeConv conv
 %name TermWf wf
 %name TermConv conv
+
+-- Well Formed Environment -----------------------------------------------------
+
+typeWfImpliesEnvWf : TypeWf env a -> EnvWf env
+typeConvImpliesEnvWf : TypeConv env a b -> EnvWf env
+termWfImpliesEnvWf : TermWf env t a -> EnvWf env
+termConvImpliesEnvWf : TermConv env t u a -> EnvWf env
-- 
cgit v1.2.3