diff options
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 |