diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Core/Declarative.idr | 36 |
1 files changed, 36 insertions, 0 deletions
diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr index 12096ac..38e6ccd 100644 --- a/src/Core/Declarative.idr +++ b/src/Core/Declarative.idr @@ -228,3 +228,39 @@ termConvRespEq (ConvConv tmConv tyConv) prf = ConvConv (termConvRespEq tmConv prf) (typeConvRespEq tyConv prf) + +-- Well-Formed Environment ----------------------------------------------------- + +export +typeWfImpliesEnvWf : TypeWf env a -> EnvWf env +export +typeConvImpliesEnvWf : TypeConv env a b -> EnvWf env +export +termWfImpliesEnvWf : TermWf env t a -> EnvWf env +export +termConvImpliesEnvWf : TermConv env t u a -> EnvWf env + +typeWfImpliesEnvWf (SetTyWf envWf) = envWf +typeWfImpliesEnvWf (PiTyWf tyWf tyWf1) = typeWfImpliesEnvWf tyWf +typeWfImpliesEnvWf (LiftWf tmWf) = termWfImpliesEnvWf tmWf + +typeConvImpliesEnvWf (ReflTy tyWf) = typeWfImpliesEnvWf tyWf +typeConvImpliesEnvWf (SymTy tyConv) = typeConvImpliesEnvWf tyConv +typeConvImpliesEnvWf (TransTy tyConv tyConv1) = typeConvImpliesEnvWf tyConv +typeConvImpliesEnvWf (PiConv tyWf tyConv tyConv1) = typeConvImpliesEnvWf tyConv +typeConvImpliesEnvWf (LiftConv tmConv) = termConvImpliesEnvWf tmConv + +termWfImpliesEnvWf (PiTmWf tmWf tmWf1) = termWfImpliesEnvWf tmWf +termWfImpliesEnvWf (VarWf envWf) = envWf +termWfImpliesEnvWf (AbsWf tyWf tmWf) = typeWfImpliesEnvWf tyWf +termWfImpliesEnvWf (AppWf tmWf tmWf1) = termWfImpliesEnvWf tmWf +termWfImpliesEnvWf (ConvWf tmWf tyConv) = termWfImpliesEnvWf tmWf + +termConvImpliesEnvWf (ReflTm tmWf) = termWfImpliesEnvWf tmWf +termConvImpliesEnvWf (SymTm tmConv) = termConvImpliesEnvWf tmConv +termConvImpliesEnvWf (TransTm tmConv tmConv1) = termConvImpliesEnvWf tmConv +termConvImpliesEnvWf (AppConv tmConv tmConv1) = termConvImpliesEnvWf tmConv +termConvImpliesEnvWf (PiTmConv tyWf tmConv tmConv1) = termConvImpliesEnvWf tmConv +termConvImpliesEnvWf (PiEta tyWf tmWf tmWf1 tmConv) = termWfImpliesEnvWf tmWf +termConvImpliesEnvWf (PiBeta tyWf tmWf tmWf1) = typeWfImpliesEnvWf tyWf +termConvImpliesEnvWf (ConvConv tmConv tyConv) = termConvImpliesEnvWf tmConv |