Data.HSet.Union

Documentation

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 Nat) (Nothing Nat)

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

(HRemove Nat els2 elsx fi, HUnionable els1 elsx elsr, (~) Bool False (Elem * e1 elsr), (~) (Maybe Nat) (Just Nat fi) (MayFstIndexSnd * ((:) * e1 els1) els2), (~) (Maybe Nat) (Nothing Nat) (MayFstIndexSnd * els2 ((:) * e1 els1))) => HUnion ((:) * e1 els1) els2 ((:) * e1 elsr) (Just Nat fi) (Nothing Nat)

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

(HUnionable els1 els2 elsr, (~) Bool False (Elem * e1 ((:) * e2 elsr)), (~) Bool False (Elem * e2 elsr), (~) (Maybe Nat) (Nothing Nat) (MayFstIndexSnd * ((:) * e1 els1) ((:) * e2 els2)), (~) (Maybe Nat) (Nothing Nat) (MayFstIndexSnd * ((:) * e2 els2) ((:) * e1 els1))) => HUnion ((:) * e1 els1) ((:) * e2 els2) ((:) * e1 ((:) * e2 elsr)) (Nothing Nat) (Nothing Nat)

(HUnionable els1 els2 elsr, (~) Bool False (Elem * e1 elsr), (~) (Maybe Nat) (Nothing Nat) (MayFstIndexSnd * ((:) * e1 els1) ((:) * e2 els2)), (~) (Maybe Nat) (Just Nat si) (MayFstIndexSnd * ((:) * e2 els2) ((:) * e1 els1))) => HUnion ((:) * e1 els1) ((:) * e2 els2) ((:) * e1 elsr) (Nothing Nat) (Just Nat si)

(HRemove Nat els2 elsx fi, HUnionable els1 elsx elsr, (~) Bool False (Elem * e1 elsr), (~) (Maybe Nat) (Just Nat (S fi)) (MayFstIndexSnd * ((:) * e1 els1) ((:) * e2 els2)), (~) (Maybe Nat) (Just Nat si) (MayFstIndexSnd * ((:) * e2 els2) ((:) * e1 els1))) => HUnion ((:) * e1 els1) ((:) * e2 els2) ((:) * e1 elsr) (Just Nat (S fi)) (Just Nat si)

(HUnionable els1 els2 elsr, (~) Bool False (Elem * e elsr)) => HUnion ((:) * e els1) ((:) * e els2) ((:) * e elsr) (Just Nat Z) (Just Nat Z)

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