Refactor `Data.Sum.{to|from}Dec` via move+deprecate in `Relation.Nullary.Decidable.Core`

agda / agda-stdlib

The Agda standard library

Other

575 stars 237 forks source link

Closed jamesmckinna closed 3 months ago

jamesmckinna commented 3 months ago

Fixes #2059 on the model of #2330 / #2336

UPDATED Added CHANGELOG : badged as v2.1 but could easily be v2.2?