diff options
Diffstat (limited to 'src/Core')
| -rw-r--r-- | src/Core/Declarative.idr | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr index 9f60d34..ae31870 100644 --- a/src/Core/Declarative.idr +++ b/src/Core/Declarative.idr @@ -286,3 +286,22 @@ CompWf (KeepWf {thin = thin2, n, prf = prf2} thinWf2) (KeepWf {thin = thin1, thi rewrite compKeep thin2 thin1 n in rewrite compAssoc thin2 thin1 thin' in KeepWf {prf = compPresNotId prf2 prf1} (CompWf thinWf2 thinWf1) + +-- Weakening Preservation ------------------------------------------------------ + +wknPresTypeWf : + TypeWf env1 a -> + ThinWf thin env2 env1 -> + TypeWf env2 (wkn a thin) +wknPresTypeConv : + TypeConv env1 a b -> + ThinWf thin env2 env1 -> + TypeConv env2 (wkn a thin) (wkn b thin) +wknPresTermWf : + TermWf env1 t a -> + ThinWf thin env2 env1 -> + TermWf env2 (wkn t thin) (wkn a thin) +wknPresTermConv : + TermConv env1 t u a -> + ThinWf thin env2 env1 -> + TermConv env2 (wkn t thin) (wkn u thin) (wkn a thin) |