Pattern matching on enums with a list of alternatives

[skeuchel]

For pattern matching on unions, we have a version that allows to provide a list of alternatives.

katamaran/theories/Syntax/Statements.v

Lines 181 to 182 in f97ef7e

	Definition stm_match_union_alt_list {Γ τ} U (s : Stm Γ (ty.union U))
	(alts : UnionAlts U Γ τ) (alts_wf : UnionAltsWf alts) : Stm Γ τ :=

This list is checked to be exhaustive by a type-level computation

katamaran/theories/Syntax/Statements.v

Lines 163 to 167 in f97ef7e

	Definition UnionAltsWf {U Γ τ} (alts : UnionAlts U Γ τ) : Prop :=
	Bool.Is_true
	(List.forallb
	(fun K => option.isSome (findUnionAlt K alts))
	(finite.enum (unionk U))).

We currently do not have the same functionality for enums which should be added.

This is useful for replacing the fixed size notations that we use, which sometimes need extension when an enum is extended, e.g. in #43, which is annoying.