Feature contract: case#

1. Lexical and grammar rules, including precedence and termination#

(case Constructor binders... . body) occurs only inside match or match-with; elsewhere case remains an ordinary identifier.

2. Scope and binding rules, including generated names#

Plain binders name constructor fields in declaration order. Their scope is the case body. Case source order is immaterial.

3. Type and quantity requirements#

The checked constructor supplies binder types and quantities. The body checks against the result of applying the eliminator motive to that constructor.

4. Effects, totality, and evaluation-order rules#

Cases are alternatives and do not impose an evaluation order on one another.

5. Elaboration into existing core or a specifically versioned new core extension#

Each case becomes one existing REliminatorBranch, in declaration order, with its arity derived from fields and recursive induction binders.

6. Representation and target support, where relevant#

No case-specific Core or runtime representation exists after elaboration.

7. Error codes and primary/secondary origins#

Unknown, duplicate, missing and arity failures use the corresponding stable ALPHA-MATCH-* code and point to the offending case or containing match.

8. Formatting and migration rules#

Formatting preserves readable cases and comments. Expanded inspection prints ordinary branch. Automatic branch migration is intentionally absent.

9. Positive, negative, execution, and edge-case tests#

tests/language/matching/ covers reordering, all coverage failures, recursive fields, source spans, Core correspondence and native execution.

10. Compatibility with the old edition, serialized forms, and cache keys#

Cases are admitted only as part of alpha-2027 matching. Their containing Match or MatchWith surface AST node owns serialization and cache identity.