diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-02 10:36:11 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-02 10:36:11 +0100 |
| commit | fbd0390f32f98dd65567bf64765bd4fbed6008b9 (patch) | |
| tree | 24611862ae362045435842953ebe146652eb96cd | |
| parent | e5771d9df3f6f980611ba32fc8f5d92343dc3f7f (diff) | |
State that weakening preserves typing.
| -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) |