Documentation

type TimesCon con = forall a b. (con a, con b) => con (a ⊗ b) :: Constraint Source #

type DualCon con = forall a. con a => con (Dual a) :: Constraint Source #

type PlusCon con = forall a b. (con a, con b) => con (a ⊕ b) :: Constraint Source #

type Con' x con = forall a b. (con a, con b) => con (a `x` b) :: Constraint Source #

type UnCon o con = forall a. con a => con (o a) :: Constraint Source #

type TimesCon1 con = forall x a b. con (a (b x)) => con ((a ⊗ b) x) :: Constraint Source #

type PlusCon1 con = forall {k} (x :: k) a b. (con (a x), con (b x)) => con ((a ⊕ b) x) :: Constraint Source #

type OneCon1 (con :: Type -> Constraint) = forall x. con x => con (One x) :: Constraint Source #

type ZeroCon1 con = forall x. con x => con (Zero x) :: Constraint Source #

reprCon :: forall con a x i t o. (Con' x con, Con' t con, con i, con o) => Repr x i t o a -> Dict (con a) Source #

reprCon1Comp :: forall (z :: Type) con (a :: Type -> Type) b. CompClosed con -> con z => CRepr a -> CRepr b -> Dict (con (a (b z))) Source #

reprCon1 :: forall (z :: Type) (con :: Type -> Constraint) a. con z => CompClosed con -> CRepr a -> Dict (con (a z)) Source #

class ProdObj (con :: k -> Constraint) where Source #

class ProdObj con => DualObj (con :: k -> Constraint) where Source #

objFstSnd :: forall con a b. ProdObj con => Dict (con (a ⊗ b)) -> Dict (con a, con b) Source #

class Trivial x Source #

data Some1 f where Source #

sizedArbRepr :: Int -> Gen (Some1 (Repr x i t o)) Source #

sizedArbSum :: Int -> Gen (Some1 (Repr x i t o)) Source #

isArbitrary1 :: CRepr x -> Dict (Arbitrary1 x) Source #

isCoArbitrary :: MRepr x -> Dict (CoArbitrary x) Source #

forallSumType :: forall {k} x i t o. (forall (a :: k). Repr x i t o a -> Property) -> Property Source #

forallType :: forall {k} x i t o. (forall (a :: k). Repr x i t o a -> Property) -> Property Source #

arbitrary2' :: forall f a b proxy. Arbitrary (f a b) => proxy a -> proxy b -> Gen (f a b) Source #

forallMorphism :: forall f a b x i t o. (Show (f a b), Arbitrary (f a b)) => Repr x i t o a -> Repr x i t o b -> (f a b -> Property) -> Property Source #