[zesterer]

They're more akin to 'destructuring' natural numbers into successors. Consider:

data Nat = Zero | Succ Nat

You could pattern match on this Nat, fetching the inner Nat, allowing the type system to prove that all cases are handled exhaustively. Arithmetic patterns just extend this notion to the built-in Nat type.

Full dependent typing is something I'd like to experiment with in time, but I'm not there yet.