Feature contract: ih#

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

(ih name) is a case-binder marker and is structural only immediately after a recursive field binder.

2. Scope and binding rules, including generated names#

name binds the recursive field's induction result in the case body. Omission creates a hygienic inaccessible NUL-prefixed binder.

3. Type and quantity requirements#

The kernel derives the induction result type from the motive and recursive field. Its quantity follows the checked eliminator branch layout.

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

The marker adds no evaluation or effect; it only chooses a source-visible name.

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

The requested name occupies the existing induction-binder position after all constructor field binders. No Core constructor is added.

6. Representation and target support, where relevant#

Erasure and targets receive the existing eliminator branch representation.

7. Error codes and primary/secondary origins#

ALPHA-MATCH-IH-POSITION points to a misplaced marker; ALPHA-MATCH-BRANCH-ARITY reports missing or extra field binders.

8. Formatting and migration rules#

Normal formatting preserves (ih name). Expanded output includes every kernel binder with fresh hygienic names. No automatic migration guesses IH intent.

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

Recursive.alpha, IHPosition.alpha, and SelfHostedBinderPlan.alpha cover explicit, omitted and misplaced induction binders in both frontend owners.

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

The marker is alpha-2027-only source syntax and disappears before checked Core; the edition-aware source cache prevents reuse under alpha-2026.