What's different to typical Algebraic-Types/Sum-Types/Nü-Enums in what they showed is that it's existing values being OR'd together, not types or new type const

What's different to typical Algebraic-Types/Sum-Types/Nü-Enums in what they showed is that it's existing values being OR'd together, not types or new type constructors. That is presumably why they are obliquely mentioning it in the comments thread of an Idris release, because Idris is known for "Dependent Types", i.e. types that depend on actual values of existing types, not just existing types.