9.3(d) was a real pain until I thought about how I'd write a function with type `(Either a b, Either a c) -> Either a (b, c)`. Before that, I kept wanting a negation operator.(EDIT: Looks like some of the exercises are getting shuffled between versions -- 9.3(d) is the one I meant as of v1.2, but that might change over time. At least the type signature is a clue about which one I mean.)

 I'm totally stuck. I would write an exhaustive pattern match to implement that function, but I have no clue how to do that in logic, without using negation.
 Right, here's my implementation in Haskell:`````` f x y = case x of Left a -> Left a Right b -> case y of Left a -> Left a Right c -> Right (b, c) `````` Each `case` represents a couple of hypothetical contexts, applying case analysis to the Either (the OR). You're going to have to duplicate some work, since the `Left a` branch appears twice and you're getting the `a` from different places.
 You know A|B and A|C. Prove A|(B&C) by assuming A and separately by assuming B, then use case analysis (by dragging the first conclusion onto the second).To prove A|(B&C) assuming B, you have to use A|C and yet another (nested) case analysis.
 Forgot to comment yesterday: thank you! Because of this I got unstuck.

Search: