Data.Metrology.Set

This module defines a few set-like operations on type-level lists. It may be applicable beyond the units package.

Documentation

type family SetEqual (as :: [k]) (bs :: [k]) :: Constraint where ...

Are two lists equal, when considered as sets?

Equations

SetEqual as bs = (Subset as bs, Subset bs as)

type family Subset (as :: [k]) (bs :: [k]) :: Constraint where ...

Is one list a subset of the other?

Equations

Subset '[] bs = () :: Constraint

Subset (a ': as) bs = (a `Elem` bs, as `Subset` bs)

type family Elem (a :: k) (bs :: [k]) :: Constraint where ...

Is an element contained in a list?

Equations

Elem a (a ': bs) = () :: Constraint

Elem a (b ': bs) = a `Elem` bs