diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-01 15:14:04 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-01 15:14:04 +0100 |
| commit | ef4dd592eea7e241583ea8c39a08092e11ef8b98 (patch) | |
| tree | 202129c71f8e21de65fe914bb7bde0ee6c3aab07 /src/Core | |
| parent | a90932302afa9e13b8ed6f1159fbe604c89d453f (diff) | |
State typing respects environment equality.
Diffstat (limited to 'src/Core')
| -rw-r--r-- | src/Core/Declarative.idr | 7 |
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 |