| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.Utils.Permutation

Synopsis

data Permutation = Perm Integer [Integer]
permute :: Permutation -> [a] -> [a]
idP :: Integer -> Permutation
composeP :: Permutation -> Permutation -> Permutation
invertP :: Permutation -> Permutation
compactP :: Permutation -> Permutation
reverseP :: Permutation -> Permutation
expandP :: Integer -> Integer -> Permutation -> Permutation
topoSort :: (a -> a -> Bool) -> [a] -> Maybe Permutation

Documentation

data Permutation | Source

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

idP :: Integer -> Permutation | Source

composeP :: Permutation -> Permutation -> Permutation | Source

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

invertP :: Permutation -> Permutation | Source

compactP :: Permutation -> Permutation | Source

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

reverseP :: Permutation -> Permutation | Source

expandP :: Integer -> Integer -> Permutation -> Permutation | Source

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

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

Stable topologic sort. The first argument decides whether its first argument is an immediate parent to its second argument.
Produced by Haddock version 2.4.2