diff options
Diffstat (limited to 'src/Core/Declarative.idr')
| -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 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 |