- -- Invariant: the list of alternatives is ALWAYS EXHAUSTIVE
- -- Invariant: the DEFAULT case must be *first*, if it occurs at all
+ -- Invariant: The list of alternatives is ALWAYS EXHAUSTIVE,
+ -- meaning that it covers all cases that can occur
+ -- See the example below
+ --
+ -- Invariant: The DEFAULT case must be *first*, if it occurs at all