Documentation

data FiniteAllFor (f :: k -> Type) (w :: k -> Type) Source #

finiteAllFor :: forall {k} (f :: k -> Type) (w :: k -> Type). FiniteAllFor f w -> AllFor f w Source #

finiteCodomain :: forall {k} (f :: k -> Type) (w :: k -> Type). FiniteAllFor f w -> [Some f] Source #

mapFiniteAllFor :: forall {k} f1 f2 (w :: k -> Type). (forall (t :: k). f1 t -> f2 t) -> FiniteAllFor f1 w -> FiniteAllFor f2 w Source #

eitherFiniteAllFor :: forall {k} (t :: k -> Type) (w1 :: k -> Type) (w2 :: k -> Type). FiniteAllFor t w1 -> FiniteAllFor t w2 -> FiniteAllFor t (EitherType w1 w2) Source #

mkFiniteAllFor :: forall {k} f w. FiniteWitness w => (forall (t :: k). w t -> f t) -> FiniteAllFor f w Source #