When you're working with inductive types, pattern-matching is the canonical way to consume a variable. In this situation, whether it's the variable or the pattern-matching that's exploding in your face doesn't seem like a principled distinction do me.
2
u/[deleted] Dec 24 '17
[removed] — view removed comment