[Haskell-cafe] Slightly Offtopic in Part

Ryan Ingram ryani.spam at gmail.com
Fri Feb 8 21:47:51 EST 2008

I'm assuming you mean the rule described in

> type Disj a b = Either a b

> disj_elim :: Disj a b -> (a -> c) -> (b -> c) -> c
> disj_elim (Left a) a2c b2c = a2c a
> disj_elim (Right b) a2c b2c = b2c b

If you know "either a is true, or b is true"
and you know "from a, I can prove c",
and you know "from b, I can prove c",
then you can prove c.

  -- ryan

On 2/8/08, PR Stanley <prstanley at ntlworld.com> wrote:
> Hi folks
> The disjunction elimination rule:
> I've been trying to make sense of it and I think I have had some
> success; however, it's far from adequate. I wonder, is there a way of
> demonstrating it in Haskell? A code frag with a jargon-free
> explanation would be mucho appreciated.
> Cheers, Paul
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe

More information about the Haskell-Cafe mailing list