diff options
| -rw-r--r-- | src/Core/Thinning.idr | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/src/Core/Thinning.idr b/src/Core/Thinning.idr index 0b1de68..a41536e 100644 --- a/src/Core/Thinning.idr +++ b/src/Core/Thinning.idr @@ -39,6 +39,10 @@ keep : sx `Thins` sy -> (0 n : Name) -> sx :< n `Thins` sy :< n keep IsId n = IsId keep (IsThinner thinner) n = IsThinner (IsKeep thinner n) +public export +wkn1 : (0 sx : Context) -> (0 n : Name) -> sx `Thins` sx :< n +wkn1 sx n = drop (id sx) n + -- Views ----------------------------------------------------------------------- public export @@ -207,3 +211,25 @@ compAssoc thin3 thin2 thin1 = compAssoc' (view thin3) (view thin2) (view thin1) export compPresNotId : IsNotId thin2 -> IsNotId thin1 -> IsNotId (thin2 . thin1) compPresNotId ItIsThinner ItIsThinner = ItIsThinner + +-- Other Properties + +export +compLeftWkn1 : + (thin : sx `Thins` sy) -> + (0 n : Name) -> + wkn1 sy n . thin = drop thin n +compLeftWkn1 thin n = Calc $ + |~ drop (id sy) n . thin + ~~ drop (id sy . thin) n ...(compLeftDrop (id sy) thin n) + ~~ drop thin n ...(cong (\thin => drop thin n) $ compLeftIdentity thin) + +export +compRightWkn1 : + (thin : sx `Thins` sy) -> + (0 n : Name) -> + keep thin n . wkn1 sx n = drop thin n +compRightWkn1 thin n = Calc $ + |~ keep thin n . drop (id sx) n + ~~ drop (thin . id sx) n ...(compRightDrop thin (id sx) n) + ~~ drop thin n ...(cong (\thin => drop thin n) $ compRightIdentity thin) |