Copyright | Copyright (C) 2015 Kyle Carter |
---|---|
License | BSD3 |
Maintainer | Kyle Carter <kylcarte@indiana.edu> |
Stability | experimental |
Portability | RankNTypes |
Safe Haskell | None |
Language | Haskell2010 |
A singleton
-esque type for representing members of finite sets,
indexed by its Nat value.
Documentation
data IFin :: N -> N -> * where Source #
Read2 N N IFin Source # | |
Show2 N N IFin Source # | |
Ord2 N N IFin Source # | |
Eq2 N N IFin Source # | |
Show1 N (IFin x) Source # | |
Ord1 N (IFin x) Source # | |
Eq1 N (IFin x) Source # | |
(~) N x' (Pred x) => Witness ØC ((~) N (S x') x) (IFin x y) Source # | An That is, |
Eq (IFin x y) Source # | |
Ord (IFin x y) Source # | |
Show (IFin x y) Source # | |
type WitnessC ØC ((~) N (S x') x) (IFin x y) Source # | |