diff options
| -rw-r--r-- | src/Core/Declarative.idr | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr index 319b465..4e849fe 100644 --- a/src/Core/Declarative.idr +++ b/src/Core/Declarative.idr @@ -189,3 +189,21 @@ termConvImpliesEnvWf (PiTermConv wf conv conv1) = termConvImpliesEnvWf conv termConvImpliesEnvWf (PiBeta wf wf1 wf2) = typeWfImpliesEnvWf wf termConvImpliesEnvWf (PiEta wf wf1 wf2 conv) = typeWfImpliesEnvWf wf termConvImpliesEnvWf (AppConv conv conv1) = termConvImpliesEnvWf conv + +-- Weakening Composition ------------------------------------------------------- + +CompWf : ThinWf thin2 env3 env2 -> ThinWf thin1 env2 env1 -> ThinWf (thin2 . thin1) env3 env1 +CompWf IdWf thinWf1 = rewrite compLeftIdentity thin1 in thinWf1 +CompWf (DropWf {thin = thin2, n} thinWf2) thinWf1 = + rewrite compLeftDrop thin2 thin1 n in + DropWf (CompWf thinWf2 thinWf1) +CompWf (KeepWf {thin = thin2, n} thinWf2) IdWf = + rewrite compRightIdentity $ keep thin2 n in + KeepWf thinWf2 +CompWf (KeepWf {thin = thin2, n} thinWf2) (DropWf {thin = thin1} thinWf1) = + rewrite compRightDrop thin2 thin1 n in + DropWf (CompWf thinWf2 thinWf1) +CompWf (KeepWf {thin = thin2, n, prf = prf2} thinWf2) (KeepWf {thin = thin1, thin', prf = prf1} thinWf1) = + rewrite compKeep thin2 thin1 n in + rewrite compAssoc thin2 thin1 thin' in + KeepWf {prf = compPresNotId prf2 prf1} (CompWf thinWf2 thinWf1) |