Documentation

eliminate2 :: Divisible f => (forall x. g x -> f x) -> g a1 -> g a2 -> f (a1, a2) Source #

eliminate3 :: Divisible f => (forall x. g x -> f x) -> g a1 -> g a2 -> g a3 -> f (a1, a2, a3) Source #

eliminate4 :: Divisible f => (forall x. g x -> f x) -> g a1 -> g a2 -> g a3 -> g a4 -> f (a1, a2, a3, a4) Source #

eliminate5 :: Divisible f => (forall x. g x -> f x) -> g a1 -> g a2 -> g a3 -> g a4 -> g a5 -> f (a1, a2, a3, a4, a5) Source #

eliminate6 :: Divisible f => (forall x. g x -> f x) -> g a1 -> g a2 -> g a3 -> g a4 -> g a5 -> g a6 -> f (a1, a2, a3, a4, a5, a6) Source #

eliminate7 :: Divisible f => (forall x. g x -> f x) -> g a1 -> g a2 -> g a3 -> g a4 -> g a5 -> g a6 -> g a7 -> f (a1, a2, a3, a4, a5, a6, a7) Source #