LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
239 stars 33 forks source link

Create `NonEmpty` instances for `EqSymbolic`, `OrdSymbolic`, `Mergeable`, etc. #688

Closed recursion-ninja closed 3 months ago

recursion-ninja commented 4 months ago

The NonEmpty data-type has been added to base for a long time and with the recent addition of the Foldable1 type-class to base, NonEmpty is receiving an implicit push for standardized usage. Unfortunately, sbv does not expose very useful type-class instances for NonEmpty making it's utilization with sbv unnecessarily cumbersome.

In a recent project I have worked on, ended up creating orphan NonEmpty instances for the following:

It would be wonderful if these (and perhaps other relevant) type-class instances can be added for NonEmpty.