Safe Haskell | None |
---|---|
Language | Haskell2010 |
Finite totally-ordered sets
Synopsis
- data Fin :: Peano -> Type where
- enum :: Natural n => List n (Fin n)
- inj₁ :: Fin n -> Fin (Succ n)
- proj₁ :: Natural n => Fin (Succ n) -> Maybe (Fin n)
- lift₁ :: (Fin m -> Fin n) -> Fin (Succ m) -> Fin (Succ n)
- fromFin :: Integral a => Fin n -> a
- toFin :: forall n a. (Natural n, Integral a) => a -> Fin (Succ n)
- toFinMay :: (Natural n, Integral a) => a -> Maybe (Fin n)
- pred :: Fin (Succ n) -> Maybe (Fin n)
Documentation
data Fin :: Peano -> Type where Source #
Totally-ordered type with n
possible values