diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-03-31 17:52:54 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-03-31 17:52:54 +0100 |
| commit | 389a38f8b114379b9ee8c37da78a4ab1986883d6 (patch) | |
| tree | 12ef50e6b385a7343bb8b5856efede135ebd52b8 /src/Core | |
| parent | a3a7020df35df764e01802089bba21079dcb0ddd (diff) | |
Define thinning composition.
Diffstat (limited to 'src/Core')
| -rw-r--r-- | src/Core/Thinning.idr | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/src/Core/Thinning.idr b/src/Core/Thinning.idr index de0d5dc..1c8f41f 100644 --- a/src/Core/Thinning.idr +++ b/src/Core/Thinning.idr @@ -57,3 +57,18 @@ view IsId = Id sx view (IsThinner (IsBase n)) = Drop IsId n view (IsThinner (IsDrop thinner n)) = Drop (IsThinner thinner) n view (IsThinner (IsKeep thinner n)) = Keep (IsThinner thinner) n ItIsThinner + +-- Operations ------------------------------------------------------------------ + +comp : Thinner sy sz -> Thinner sx sy -> sx `Thins` sz +comp (IsBase n) thinner1 = drop (IsThinner thinner1) n +comp (IsDrop thinner2 n) thinner1 = drop (comp thinner2 thinner1) n +comp (IsKeep thinner2 n) (IsBase n) = drop (IsThinner thinner2) n +comp (IsKeep thinner2 n) (IsDrop thinner1 n) = drop (comp thinner2 thinner1) n +comp (IsKeep thinner2 n) (IsKeep thinner1 n) = keep (comp thinner2 thinner1) n + +export +(.) : sy `Thins` sz -> sx `Thins` sy -> sx `Thins` sz +IsId . thin1 = thin1 +(IsThinner thinner2) . IsId = IsThinner thinner2 +(IsThinner thinner2) . (IsThinner thinner1) = comp thinner2 thinner1 |