-- 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.9.0


-- | Lists of statically-known length
module Data.Fin.List
data Peano

-- | A list of exactly <tt>n</tt> values of type <tt>a</tt>
data List n a
[Nil] :: List Zero a
[:.] :: a -> List n a -> List (Succ n) a
infixr 5 :.
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

-- | Bring givenly many elements from the tail of the list to the front.
rotate :: Fin n -> List n a -> List n a

-- | Focalize on the giventh element.
at :: Functor f => Fin n -> (a -> f a) -> List n a -> f (List n a)

-- | Swap the 2 giventh elements of the list.
swap :: Fin n -> Fin n -> List n a -> List n a
(!!) :: List n a -> Fin n -> a

-- | Find the indices of all elements satisfying the given predicate,
--   gathering them in <tt>p</tt>.
findIndex :: Alternative p => (a -> Bool) -> List n a -> p (Fin n)


-- | Finite totally-ordered sets
module Data.Fin

-- | Totally-ordered type with <tt>n</tt> possible values
data Fin :: Peano -> Type
[Zero] :: Fin (Succ n)
[Succ] :: Fin n -> Fin (Succ n)

-- | Enumerate all values of type <tt><a>Fin</a> n</tt>, in ascending
--   order.
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

-- | Convert to <a>Fin</a>, modulo <tt>n</tt>.
toFin :: forall n a. (Natural n, Integral a) => a -> Fin (Succ n)

-- | Convert to <a>Fin</a>, failing if the argument is out of bounds.
toFinMay :: (Natural n, Integral a) => a -> Maybe (Fin n)
pred :: Fin (Succ n) -> Maybe (Fin n)


-- | See <a>Permutation</a>
module Data.Fin.Permutation

-- | Permutation of <tt>n</tt> elements
--   
--   Any permutation can be expressed as a product of transpositions. Ergo,
--   construct with <a>Semigroup</a> operations and <a>swap</a>.
data Permutation n
apply :: Permutation n -> List n a -> List n a
unapply :: Permutation n -> List n a -> List n a

-- | Transposition of the giventh elements
swap :: Natural n => Fin n -> Fin n -> Permutation n

-- | Orbit of the given index under the given permutation
orbit :: Natural n => Permutation n -> Fin n -> NonEmpty (Fin n)

-- | All the cycles of the given permutation, which are necessarily
--   disjoint
cycles :: forall n. Natural n => Permutation (Succ n) -> NonEmpty (NonEmpty (Fin (Succ n)))
instance GHC.Base.Functor Data.Fin.Permutation.Stream
instance GHC.Classes.Eq (Data.Fin.Permutation.Permutation n)
instance GHC.Show.Show (Data.Fin.Permutation.Permutation n)
instance Data.Natural.Class.Natural n => GHC.Base.Semigroup (Data.Fin.Permutation.Permutation n)
instance Data.Natural.Class.Natural n => Data.Universe.Class.Universe (Data.Fin.Permutation.Permutation n)
instance Data.Natural.Class.Natural n => Data.Universe.Class.Finite (Data.Fin.Permutation.Permutation n)
instance Data.Natural.Class.Natural n => GHC.Base.Monoid (Data.Fin.Permutation.Permutation n)
instance Data.Natural.Class.Natural n => Algebra.Group (Data.Fin.Permutation.Permutation n)