From b6fc70ab061b10983458d6331685c111b47af75b Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Sat, 1 Apr 2023 14:57:08 +0100 Subject: Make type of comp more precise. This is in anticipation of a proof that composition preserves IsNotId. --- src/Core/Thinning.idr | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'src') 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 ------------------------------------------------------ -- cgit v1.2.3