diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-15 17:37:45 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-15 17:37:45 +0100 |
| commit | dc9aa0cc59d67690e7eba1543a37c397e751429a (patch) | |
| tree | 8ec9c249050ecde5e6d6e08249ce53b4c54329c2 | |
| parent | bd2497f868f7549e4b26e1b142d193d07e528f4e (diff) | |
Prove environments are well-formed.
| -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 |