Dependently typed elimination functions using singletons https://github.com/RyanGlScott/eliminators

Version on this page:0.3
LTS Haskell 12.2:0.4.1
Stackage Nightly 2018-07-21:0.4.1
Latest on Hackage:0.4.1

See all snapshots eliminators appears in

BSD3 licensed by Ryan Scott
Maintained by Ryan Scott

Module documentation for 0.3


Hackage Hackage Dependencies Haskell Programming Language BSD3 License Build

This library provides eliminators for inductive data types, leveraging the power of the singletons library to allow dependently typed elimination.


0.4.1 [2018.02.13]

  • Add elimVoid to Data.Eliminator.

0.4 [2018.01.09]

  • Require singletons-2.4 and GHC 8.4.

0.3 [2017-11-07]

  • Migrate the old elimNat from Data.Eliminator (which worked over the Nat from GHC.TypeNats) to Data.Eliminator.TypeNats. There elimNat that now lives in Data.Eliminator is for an unrelated Nat data type from the singleton-nats package (which is a proper, inductively defined, Peano natural number type).

0.2 [2017-07-22]

  • Introduce the Data.Eliminator.TH module, 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 (~>).

0.1 [2017-07-02]

  • Initial release.
comments powered byDisqus