http://hackage.haskell.org/package/eliminators "eliminators package on Hackage" [Haskell.org]: http://www.haskell.org "The Haskell Programming Language" [tl;dr Legal: BSD3]: https://tldrlegal.com/license/bsd-3-clause-license-%28revised%29 "BSD 3-Clause License (Revised)"
This library provides eliminators for inductive data types, leveraging the power of the
singletons library to allow dependently typed elimination.
singletons-2.4and GHC 8.4.
Migrate the old
Data.Eliminator(which worked over the
elimNatthat now lives in
Data.Eliminatoris for an unrelated
Natdata type from the
singleton-natspackage (which is a proper, inductively defined, Peano natural number type).
- Introduce the
Data.Eliminator.THmodule, which provides functionality for generating eliminator functions using Template Haskell. Currently, only simple algebraic data types that do not use polymorphic recursion are supported.
- All eliminators now use predicates with
- Initial release.