Relation.Binary.Sum/Product being removed from the standard library #3
Description
Just a heads-up that Relation.Binary.Sum/Product which was deprecated a couple of years back will be removed in the upcoming v1.0 of the standard library. You should use Data.Sum/Product.Relation.Binary.Pointwise instead.
The following files will need to be changed:
https://github.com/crypto-agda/explore/blob/master/lib/Explore/Sum.agda
https://github.com/crypto-agda/explore/blob/master/lib/Explore/Old/Sum/sum-properties-setoid.agda