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.
- data IFin :: N -> N -> * where
- class LTC x y => LessEq x y where
- type LTC x y :: Constraint
- liftIFin :: IFin x z -> IFin y z
- ifinZ :: IFin Z x -> Void
- weaken :: IFin x y -> IFin (S x) y
- ifinNat :: IFin x y -> Nat y
- ifinVal :: IFin x y -> Int
- onIFinPred :: (forall x. IFin m x -> IFin n x) -> IFin (S m) y -> IFin (S n) y
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) = (~) N x' (Pred x) Source |