nub package:Agda

The nub function removes duplicate elements from a list. In particular, it keeps only the first occurrence of each element. (The name nub means 'essence'.) It is a special case of nubBy, which allows the programmer to supply their own inequality test.

Partition a list into first and later occurrences of elements (modulo some quotient given by a representation function). Time: O(n log n). Specification:

nubAndDuplicatesOn f xs = (ys, xs List.\\ ys)
where ys = nubOn f xs

A variant of nubOn that is parametrised by a function that is used to select which element from a group of equal elements that is returned. The returned elements keep the order that they had in the input list. Precondition: The length of the input list must be at most maxBound :: Int.

Non-efficient, monadic nub. O(n²).

Efficient variant of nubBy for lists, using a set to store already seen elements. O(n log n) Specification:

nubOn f xs == 'nubBy' ((==) `'on'` f) xs.

The nubBy function behaves just like nub, except it uses a user-supplied equality predicate instead of the overloaded == function.

Non-efficient, monadic nub. O(n²).