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 [-]