Data.Collections.Analysis

Definitions

transitiveClosureM : Monad m => Eq a => (a -> m (List a)) -> List a -> m (List a)

Visibility: export

holdsOnAnyInTrCl : Monad m => Eq a => (a -> Bool) -> (a -> m (List a)) -> List a -> m Bool

Visibility: export

partitionEithersPos : Vect n (Either a b) -> (List a, (List b, FinSet n))

Totality: total
Visibility: export

joinEithersPos : (as : List a) -> (bs : List b) -> FinSet (as .length + bs .length) -> Maybe (Vect (as .length + bs .length) (Either a b))

Totality: total
Visibility: export

disjointDepSets : DVect n (FinSet . finToNat) -> FinSet n -> List (FinSet n)

Totality: total
Visibility: export

combinations : Vect n (List1 a) -> List1 (Vect n a)

Totality: total
Visibility: public export

permutations : Ord a => SortedSet a -> List1 (List a)

Totality: total
Visibility: export

permutationsFin : FinSet n -> List1 (List (Fin n))

Totality: total
Visibility: export

permutations' : Ord a => SortedSet a -> List (List a)

Totality: total
Visibility: public export

indepPermutations : List (FinSet n) -> FinSet n -> List1 (List (Fin n))

Totality: total
Visibility: export

indepPermutations' : List (FinSet n) -> FinSet n -> List (List (Fin n))

Totality: total
Visibility: public export