Agda.Utils.Permutation

Documentation

data Permutation

permute [2,3,1] [x,y,z] = [y,z,x]

Constructors

Perm Integer [Integer]

Instances

Eq Permutation

Data Permutation

Show Permutation

Typeable Permutation

Sized Permutation

Abstract Permutation

Apply Permutation

EmbPrj Permutation

permute :: Permutation -> [a] -> [a]

permute [2,3,1] [x1,x2,x3] = [x2,x3,x1] More precisely, permute indices list = sublist, generates sublist from list by picking the elements of list as indicated by indices. permute [2,4,1] [x1,x2,x3,x4] = [x2,x4,x1]

idP :: Integer -> Permutation

takeP :: Integer -> Permutation -> Permutation

composeP :: Permutation -> Permutation -> Permutation

permute (compose p1 p2) == permute p1 . permute p2

invertP :: Permutation -> Permutation

compactP :: Permutation -> Permutation

Turn a possible non-surjective permutation into a surjective permutation.

reverseP :: Permutation -> Permutation

expandP :: Integer -> Integer -> Permutation -> Permutation

expandP i n  in the domain of  replace the ith element by n elements.

topoSort :: (a -> a -> Bool) -> [a] -> Maybe Permutation

Stable topologic sort. The first argument decides whether its first argument is an immediate parent to its second argument.