diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-01 14:57:08 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-01 14:57:08 +0100 |
| commit | b6fc70ab061b10983458d6331685c111b47af75b (patch) | |
| tree | c73d63f7838cc2fbba650e50976cecf5dbde2a34 /src/Core | |
| parent | 5bcb0623a1b15aa2a46ab3a922c0f4b500d7d8e6 (diff) | |
Make type of comp more precise.
This is in anticipation of a proof that composition preserves IsNotId.
Diffstat (limited to 'src/Core')
| -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 ------------------------------------------------------ |