Data.HSet.Union

Documentation

type family MayFstIndexSnd ts1 ts2 :: Maybe N

Equations

MayFstIndexSnd (e : els) x = IndexOfMay e x

MayFstIndexSnd `[]` x = Nothing

class (fidx ~ MayFstIndexSnd els1 els2, sidx ~ MayFstIndexSnd els2 els1) => HUnion els1 els2 elsr fidx sidx | els1 els2 fidx sidx -> elsr where

Methods

hunion :: HSet els1 -> HSet els2 -> HSet elsr

Instances

HUnion ([] *) ([] *) ([] *) (Nothing N) (Nothing N)

HUnion ([] *) ((:) * e els) ((:) * e els) (Nothing N) (Nothing N)

(HRemove N els2 elsx fi, HUnionable els1 elsx elsr, NotElem * e1 elsr, (~) (Maybe N) (Just N fi) (MayFstIndexSnd * ((:) * e1 els1) els2), (~) (Maybe N) (Nothing N) (MayFstIndexSnd * els2 ((:) * e1 els1))) => HUnion ((:) * e1 els1) els2 ((:) * e1 elsr) (Just N fi) (Nothing N)

HUnion ((:) * e els) ([] *) ((:) * e els) (Nothing N) (Nothing N)

(HUnionable els1 els2 elsr, NotElem * e1 ((:) * e2 elsr), NotElem * e2 elsr, (~) (Maybe N) (Nothing N) (MayFstIndexSnd * ((:) * e1 els1) ((:) * e2 els2)), (~) (Maybe N) (Nothing N) (MayFstIndexSnd * ((:) * e2 els2) ((:) * e1 els1))) => HUnion ((:) * e1 els1) ((:) * e2 els2) ((:) * e1 ((:) * e2 elsr)) (Nothing N) (Nothing N)

(HUnionable els1 els2 elsr, NotElem * e1 elsr, (~) (Maybe N) (Nothing N) (MayFstIndexSnd * ((:) * e1 els1) ((:) * e2 els2)), (~) (Maybe N) (Just N si) (MayFstIndexSnd * ((:) * e2 els2) ((:) * e1 els1))) => HUnion ((:) * e1 els1) ((:) * e2 els2) ((:) * e1 elsr) (Nothing N) (Just N si)

(HRemove N els2 elsx fi, HUnionable els1 elsx elsr, NotElem * e1 elsr, (~) (Maybe N) (Just N (S fi)) (MayFstIndexSnd * ((:) * e1 els1) ((:) * e2 els2)), (~) (Maybe N) (Just N si) (MayFstIndexSnd * ((:) * e2 els2) ((:) * e1 els1))) => HUnion ((:) * e1 els1) ((:) * e2 els2) ((:) * e1 elsr) (Just N (S fi)) (Just N si)

(HUnionable els1 els2 elsr, NotElem * e elsr) => HUnion ((:) * e els1) ((:) * e els2) ((:) * e elsr) (Just N Z) (Just N Z)

type HUnionable els1 els2 elsr = HUnion els1 els2 elsr (MayFstIndexSnd els1 els2) (MayFstIndexSnd els2 els1)