# Data.Fin: exported symbols usage examples

## Symbols

• enum See 3 Occurences [+] Collapse [-]
Found in Data.Fin.Permutation from the package Fin
```swap :: Natural n => Fin n -> Fin n -> Permutation n
swap = unOp₂ \$ natural (Op₂ \$ \ case) \$ Op₂ . curry \$ \ case
(Zero, Zero) -> mempty
(Succ m, Succ n) -> PS Zero (swap m n)
(Zero, Succ n) -> PS (Succ n) mempty
(Succ m, Zero) -> PS (Succ m) mempty

newtype Op₂ a b n = Op₂ { unOp₂ :: a n -> a n -> b n }

orbit :: Natural n => Permutation n -> Fin n -> NonEmpty (Fin n)
orbit p n = case (!! n) <\$> iterate (apply p) enum of
a:<as -> a:|takeWhile (/= a) as

cycles :: ∀ n . Natural n => Permutation (P.Succ n) -> NonEmpty (NonEmpty (Fin (P.Succ n)))
cycles p = nubOn minimum \$ orbit p <\$> case enum @(P.Succ n) of n:.ns -> n:|toList ns

infixr 5 :<
data Stream a = a :< Stream a
deriving (Functor)
```

Found in Data.Fin.Permutation from the package Fin
```        go (PS n p) = (ms, PS m q)
where (ns, q) = go p
ms@(m:._) = L.swap Zero n \$ Zero:.(Succ <\$> ns)

swap :: Natural n => Fin n -> Fin n -> Permutation n
swap = unOp₂ \$ natural (Op₂ \$ \ case) \$ Op₂ . curry \$ \ case
(Zero, Zero) -> mempty
(Succ m, Succ n) -> PS Zero (swap m n)
(Zero, Succ n) -> PS (Succ n) mempty
(Succ m, Zero) -> PS (Succ m) mempty

newtype Op₂ a b n = Op₂ { unOp₂ :: a n -> a n -> b n }

orbit :: Natural n => Permutation n -> Fin n -> NonEmpty (Fin n)
orbit p n = case (!! n) <\$> iterate (apply p) enum of
a:<as -> a:|takeWhile (/= a) as

cycles :: ∀ n . Natural n => Permutation (P.Succ n) -> NonEmpty (NonEmpty (Fin (P.Succ n)))
cycles p = nubOn minimum \$ orbit p <\$> case enum @(P.Succ n) of n:.ns -> n:|toList ns
```

Found in Data.Fin.Permutation from the package Fin
```import Data.Functor.Compose (Compose (..))
import Data.List.NonEmpty (NonEmpty (..))
import Data.Natural.Class (Natural (..))
import qualified Data.Peano as P
import Data.Universe.Class

data Permutation n where
PZ :: Permutation P.Zero
PS :: Fin (P.Succ n) -> Permutation n -> Permutation (P.Succ n)

deriving instance Eq (Permutation n)
deriving instance Show (Permutation n)

instance Natural n => Universe (Permutation n) where
universe = getCompose \$ natural (Compose [PZ]) (Compose \$ PS <\$> toList enum <*> universe)

instance Natural n => Finite (Permutation n)

apply :: Permutation n -> List n a -> List n a
apply PZ Nil = Nil
```

fromFin No usage example found for this symbol :( Collapse [-]
inj₁ No usage example found for this symbol :( Collapse [-]
lift₁ No usage example found for this symbol :( Collapse [-]
toFin No usage example found for this symbol :( Collapse [-]
toFinMay No usage example found for this symbol :( Collapse [-]
Fin No usage example found for this symbol :( Collapse [-]