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.
Documentation
data Fin :: N -> * where Source #
Read1 N Fin Source # | |
Show1 N Fin Source # | |
Ord1 N Fin Source # | |
Eq1 N Fin Source # | |
(~) N n' (Pred n) => Witness ØC ((~) N (S n') n) (Fin n) Source # | A That is, |
(Known N Nat n, Pos n) => Bounded (Fin n) Source # | |
(Known N Nat n, Pos n) => Enum (Fin n) Source # | |
Eq (Fin n) Source # | |
Ord (Fin n) Source # | |
Show (Fin n) Source # | |
type WitnessC ØC ((~) N (S n') n) (Fin n) Source # | |