I'm assuming you mean the rule described in http://en.wikibooks.org/wiki/Formal_Logic/Sentential_Logic/Inference_Rules
> 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 <[EMAIL PROTECTED]> 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@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe