diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Core/Thinning.idr | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/Core/Thinning.idr b/src/Core/Thinning.idr index e70cf56..ecc3f47 100644 --- a/src/Core/Thinning.idr +++ b/src/Core/Thinning.idr @@ -62,18 +62,18 @@ view (IsThinner (IsKeep thinner n)) = Keep (IsThinner thinner) n -- 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 +comp : Thinner sy sz -> Thinner sx sy -> Thinner sx sz +comp (IsBase n) thinner1 = IsDrop thinner1 n +comp (IsDrop thinner2 n) thinner1 = IsDrop (comp thinner2 thinner1) n +comp (IsKeep thinner2 n) (IsBase n) = IsDrop thinner2 n +comp (IsKeep thinner2 n) (IsDrop thinner1 n) = IsDrop (comp thinner2 thinner1) n +comp (IsKeep thinner2 n) (IsKeep thinner1 n) = IsKeep (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 +(IsThinner thinner2) . (IsThinner thinner1) = IsThinner (comp thinner2 thinner1) -- Composition Properties ------------------------------------------------------ |