-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Finite totally-ordered sets
--   
--   Finite totally-ordered sets
@package Fin
@version 0.2.2.0

module Data.Fin.List
data Peano :: *
data List n a
[Nil] :: List Zero a
[:.] :: a -> List n a -> List (Succ n) a
fromList :: Natural n => [a] -> Maybe (List n a)
uncons :: List (Succ n) a -> (a, List n a)
head :: List (Succ n) a -> a
tail :: List (Succ n) a -> List n a
init :: List (Succ n) a -> List n a
last :: List (Succ n) a -> a
reverse :: List n a -> List n a
at :: Functor f => Fin n -> (a -> f a) -> List n a -> f (List n a)
swap :: Fin n -> Fin n -> List n a -> List n a
(!!) :: List n a -> Fin n -> a

module Data.Fin
data Fin :: Peano -> *
[Zero] :: Fin (Succ n)
[Succ] :: Fin n -> Fin (Succ n)
enum :: Natural n => List n (Fin n)
inj₁ :: Fin n -> Fin (Succ 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 (Succ n))