4 ms·
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.
by GolDDranks 8y ago
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.
- mbrock 8y agoYou 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.
- GolDDranks 8y agoForgot to comment yesterday: thank you! Because of this I got unstuck.
- Twisol 8y agoRight, 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.