eliminators
Version 0.9.5 revision 1 uploaded by ryanglscott.
Package meta
- Synopsis
- Dependently typed elimination functions using singletons
- Description
This library provides eliminators for inductive data types, leveraging the power of the
singletonslibrary to allow dependently typed elimination.- Author
- Ryan Scott
- Bug reports
- https://github.com/RyanGlScott/eliminators/issues
- Category
- Dependent Types
- Copyright
- (C) 2017 Ryan Scott
- Homepage
- https://github.com/RyanGlScott/eliminators
- Maintainer
- Ryan Scott <ryan.gl.scott@gmail.com>
- Package URL
- n/a
- Stability
- Experimental