State typing respects environment equality.

1 files changed, 7 insertions, 0 deletions

diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr
index 4e849fe..b90bf20 100644
--- a/src/Core/Declarative.idr
+++ b/src/Core/Declarative.idr
@@ -158,6 +158,13 @@ data ThinWf : sx `Thins` sy -> Env sy -> Env sx -> Type where
 
 %name ThinWf thinWf
 
+-- Environment Equality --------------------------------------------------------
+
+typeWfRespEnvEq : TypeWf env1 a -> EnvEq env1 env2 -> TypeWf env2 a
+typeConvRespEnvEq : TypeConv env1 a b -> EnvEq env1 env2 -> TypeConv env2 a b
+termWfRespEnvEq : TermWf env1 t a -> EnvEq env1 env2 -> TermWf env2 t a
+termConvRespEnvEq : TermConv env1 t u b -> EnvEq env1 env2 -> TermConv env2 t u b
+
 -- Well Formed Environment -----------------------------------------------------
 
 typeWfImpliesEnvWf : TypeWf env a -> EnvWf env