Data.Fin.List: exported symbols usage examples

Symbols

  • !! No usage example found for this symbol :( Collapse [-]
    at See 2 Occurences [+] Collapse [-]
    Found in Data.Fin.Permutation from the package Fin
    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
    apply (PS Zero p) (a:.as) = a:.apply p as
    apply (PS (Succ n) p) (a:.as) = uncurry (:.) $ at n (flip (,) a) (apply p as)
    
    unapply :: Permutation n -> List n a -> List n a
    unapply PZ Nil = Nil
    unapply (PS Zero p) (a:.as) = a:.unapply p as
    unapply (PS (Succ n) p) (a:.as) = unapply (PS Zero p) . uncurry (:.) $ at n (flip (,) a) as
    
    instance Natural n => Semigroup (Permutation n) where
        (<>) = unOp₂ $ natural (Op₂ . curry $ \ (PZ, PZ) -> PZ) $ Op₂ . curry $ \ case
            (PS m p, PS Zero q) -> PS m (p <> q)
            (PS m p, PS n q) -> case invert (PS n (invert p)) of
    

    Found in Data.Fin.Permutation from the package Fin
        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
    apply (PS Zero p) (a:.as) = a:.apply p as
    apply (PS (Succ n) p) (a:.as) = uncurry (:.) $ at n (flip (,) a) (apply p as)
    
    unapply :: Permutation n -> List n a -> List n a
    unapply PZ Nil = Nil
    unapply (PS Zero p) (a:.as) = a:.unapply p as
    unapply (PS (Succ n) p) (a:.as) = unapply (PS Zero p) . uncurry (:.) $ at n (flip (,) a) as
    

    fromList No usage example found for this symbol :( Collapse [-]
    head No usage example found for this symbol :( Collapse [-]
    init No usage example found for this symbol :( Collapse [-]
    last No usage example found for this symbol :( Collapse [-]
    reverse No usage example found for this symbol :( Collapse [-]
    rotate No usage example found for this symbol :( Collapse [-]
    swap See 7 Occurences [+] Collapse [-]
    Found in Data.Fin.Permutation from the package Fin
        mempty = natural PZ $ PS Zero mempty
    
    instance Natural n => Group (Permutation n) where
        invert = snd . go
          where
            go ::  n . Permutation n -> (List n (Fin n), Permutation n)
            go PZ = (Nil, PZ)
            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 }
    

    Found in Data.Fin.Permutation from the package Fin
    instance Natural n => Monoid (Permutation n) where
        mempty = natural PZ $ PS Zero mempty
    
    instance Natural n => Group (Permutation n) where
        invert = snd . go
          where
            go ::  n . Permutation n -> (List n (Fin n), Permutation n)
            go PZ = (Nil, PZ)
            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
    

    Found in Data.Fin.Permutation from the package Fin
                    (Succ m, Succ o) -> PS (Succ o) (swap m o <> r <> q)
    
    instance Natural n => Monoid (Permutation n) where
        mempty = natural PZ $ PS Zero mempty
    
    instance Natural n => Group (Permutation n) where
        invert = snd . go
          where
            go ::  n . Permutation n -> (List n (Fin n), Permutation n)
            go PZ = (Nil, PZ)
            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
    

    Found in Data.Fin.Permutation from the package Fin
                    (Zero, _) -> PS o (r <> q)
                    (_, Zero) -> PS m (r <> q)
                    (Succ m, Succ o) -> PS (Succ o) (swap m o <> r <> q)
    
    instance Natural n => Monoid (Permutation n) where
        mempty = natural PZ $ PS Zero mempty
    
    instance Natural n => Group (Permutation n) where
        invert = snd . go
          where
            go ::  n . Permutation n -> (List n (Fin n), Permutation n)
            go PZ = (Nil, PZ)
            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)
    

    Found in Data.Fin.Permutation from the package Fin
    apply (PS (Succ n) p) (a:.as) = uncurry (:.) $ at n (flip (,) a) (apply p as)
    
    unapply :: Permutation n -> List n a -> List n a
    unapply PZ Nil = Nil
    unapply (PS Zero p) (a:.as) = a:.unapply p as
    unapply (PS (Succ n) p) (a:.as) = unapply (PS Zero p) . uncurry (:.) $ at n (flip (,) a) as
    
    instance Natural n => Semigroup (Permutation n) where
        (<>) = unOp₂ $ natural (Op₂ . curry $ \ (PZ, PZ) -> PZ) $ Op₂ . curry $ \ case
            (PS m p, PS Zero q) -> PS m (p <> q)
            (PS m p, PS n q) -> case invert (PS n (invert p)) of
                PS o r -> case (m, o) of
                    (Zero, _) -> PS o (r <> q)
                    (_, Zero) -> PS m (r <> q)
                    (Succ m, Succ o) -> PS (Succ o) (swap m o <> r <> q)
    
    instance Natural n => Monoid (Permutation n) where
        mempty = natural PZ $ PS Zero mempty
    
    instance Natural n => Group (Permutation n) where
    

    Found in Data.Fin.Permutation from the package Fin
    {-# LANGUAGE TypeApplications #-}
    
    module Data.Fin.Permutation (Permutation, apply, unapply, swap, orbit, cycles) where
    
    import Prelude (Functor (..), Applicative (..), Eq (..), Show (..), Bool (..), ($), (<$>), otherwise, snd, flip, curry, uncurry)
    import Algebra
    import Control.Category (Category (..))
    import Data.Fin
    import Data.Fin.List hiding (swap)
    import qualified Data.Fin.List as L
    import Data.Foldable (elem, minimum, toList)
    import Data.Functor.Compose (Compose (..))
    import Data.List.NonEmpty (NonEmpty (..))
    import Data.Natural.Class (Natural (..))
    

    Found in Data.Fin.Permutation from the package Fin
    {-# LANGUAGE TypeApplications #-}
    
    module Data.Fin.Permutation (Permutation, apply, unapply, swap, orbit, cycles) where
    
    import Prelude (Functor (..), Applicative (..), Eq (..), Show (..), Bool (..), ($), (<$>), otherwise, snd, flip, curry, uncurry)
    import Algebra
    import Control.Category (Category (..))
    import Data.Fin
    

    tail No usage example found for this symbol :( Collapse [-]
    uncons No usage example found for this symbol :( Collapse [-]
    List No usage example found for this symbol :( Collapse [-]
    Peano No usage example found for this symbol :( Collapse [-]