Feature contract: match-with#

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

(match-with Family motive scrutinee cases...) is a parenthesized prefix form.

2. Scope and binding rules, including generated names#

The motive is outside case scope. Case field and (ih name) binders follow the same rules as match.

3. Type and quantity requirements#

The motive has the checked index telescope followed by the matched family value. It is required when the result depends on the scrutinee or its indices.

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

The scrutinee is evaluated once; cases remain kernel-checked alternatives.

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

The form lowers to the existing exhaustive REliminate, retaining the supplied motive and ordering cases by the family declaration.

6. Representation and target support, where relevant#

No Core or runtime representation is added; existing eliminator support applies.

7. Error codes and primary/secondary origins#

Motive type failures retain the motive span. Coverage and binder failures use the ALPHA-MATCH-* codes listed in match.

8. Formatting and migration rules#

Normal formatting preserves match-with; expanded inspection emits checked eliminate. There is no automatic migration from an arbitrary eliminator.

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

tests/language/matching/IndexedMotive.alpha checks an indexed recursive family; the matching harness checks formatting, expansion, origins and native execution.

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

alpha-2026 rejects the source form. Tags 25 and 26 extend the surface AST checkpoint codec; checked Core remains compatible and edition-keyed.