Feature contract: let*#

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

(let* (QUANTITY NAME = VALUE) ... in BODY) is a parenthesized prefix form with one or more bindings. A binding may insert : TYPE before =. let* is one lexical head; * is not admitted in ordinary identifiers.

2. Scope and binding rules, including generated names#

Bindings are ordered. Each name is in scope in later annotations, later values, and the body, and is absent from its own annotation and value. The form creates no generated source-visible names.

3. Type and quantity requirements#

An annotated value checks against its annotation; an omitted annotation is inferred once. Every binding retains its declared erased, affine, linear, or unrestricted quantity. The trusted kernel enforces that quantity in the remaining bindings and body.

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

Bindings evaluate from left to right under the existing core-let semantics. Each bound expression occurs once in core. Referencing its binder does not substitute another copy of the expression. The form adds no effects or partiality.

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

The surface form folds right into nested existing RLet nodes. It is not translated into lambda application or source substitution.

6. Representation and target support, where relevant#

Checked interfaces, erasure, and x86-64 compilation receive the same core-let chain as explicit let. No ALRI or artifact schema changes.

7. Error codes and primary/secondary origins#

ALPHA-PARSE-LET-STAR covers a missing binding or unterminated form. Existing parse, type, and ALPHA-QUANTITY-VIOLATION diagnostics retain the binding or body origin that caused them.

8. Formatting and migration rules#

Canonical formatting keeps let*, one binding per line, comments, and an indented in body. Expanded inspection prints nested let. There is no automatic migration from arbitrary nested lets because comments and authorial grouping cannot always be recovered safely.

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

tests/language/sequencing/ covers inferred and typed chains, exact core correspondence, native execution, an eight-use shared DAG, a killed substitution mutant, and linear rejection. debug/sequence-format-check.py records elaborated-core bytes and normalized erased-runtime nodes.

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

alpha-2026 rejects let*; alpha-2027 admits it. Expanded explicit let remains valid in the old edition. The edition participates in cache identity; the core and checked-interface schemas do not change.