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 bs :: Constraint

Are two lists equal, when considered as sets?

Equations

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

type family Subset as bs :: Constraint

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 bs :: Constraint

Is an element contained in a list?

Equations

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

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