Follow-up question: how do you know that in the natural number case you need to wrap each subpattern inside {:nat, val} but you don’t have to in the maybe case? Given one says zero(0) and the other says nothing(nil), I was expecting zero() to generate 0 and not {:nat, 0}.
I also assume that when using unions you can no longer do something like def value(maybe())? I guess not doing that makes sense though, as the different subpatterns may have different shapes/number of arguments.
