diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-06-01 17:07:41 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-06-01 17:07:41 +0100 |
| commit | d5f8497dbb6de72d9664f48d6acbc9772de77be3 (patch) | |
| tree | e1a4aeb598d263af3d888f8c0c68c07f15d13f14 /src/Thinning.idr | |
| parent | 3eb03e2347b35432f7eae7d6847ec9ecf1dff19e (diff) | |
Give a logical relation template.
Diffstat (limited to 'src/Thinning.idr')
| -rw-r--r-- | src/Thinning.idr | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/Thinning.idr b/src/Thinning.idr index 0e99711..a79f0f5 100644 --- a/src/Thinning.idr +++ b/src/Thinning.idr @@ -142,3 +142,12 @@ keepHomo (Drop thin2) (Keep thin1) = Refl keepHomo (Keep thin2) Id = Refl keepHomo (Keep thin2) (Drop thin) = Refl keepHomo (Keep thin2) (Keep thin) = Refl + +export +keepDrop : + (thin2 : sy `Thins` sz) -> + (thin1 : sx `Thins` sy) -> + keep thin2 . Drop thin1 = Drop (thin2 . thin1) +keepDrop Id thin1 = Refl +keepDrop (Drop thin2) thin1 = Refl +keepDrop (Keep thin2) thin1 = Refl |