diff --git a/CHANGELOG.md b/CHANGELOG.md index ba2866023..55ef74a42 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -232,6 +232,8 @@ were made to be indeed lazy by the effect, but their requirements were strengthened from `Applicative` to `Monad`. +* Implements `Sized` for `Data.Seq.Sized` and `Data.Seq.Unsized`. + #### Papers * In `Control.DivideAndConquer`: a port of the paper diff --git a/libs/contrib/Data/Seq/Sized.idr b/libs/contrib/Data/Seq/Sized.idr index 748363844..43578cbd7 100644 --- a/libs/contrib/Data/Seq/Sized.idr +++ b/libs/contrib/Data/Seq/Sized.idr @@ -207,3 +207,7 @@ public export implementation {n : Nat} -> Applicative (Seq n) where pure = replicate n (<*>) = zipWith ($) + +public export +implementation Sized (Seq n a) where + size (MkSeq s) = size s diff --git a/libs/contrib/Data/Seq/Unsized.idr b/libs/contrib/Data/Seq/Unsized.idr index b4b850fd7..cb0eb28f5 100644 --- a/libs/contrib/Data/Seq/Unsized.idr +++ b/libs/contrib/Data/Seq/Unsized.idr @@ -218,3 +218,7 @@ public export public export implementation Monad Seq where xs >>= f = foldMap f xs + +public export +implementation Sized (Seq a) where + size (MkSeq s) = size s