diff --git a/NEXT.md b/NEXT.md
index 7c1f927..675bea7 100644
--- a/NEXT.md
+++ b/NEXT.md
@@ -225,10 +225,32 @@ Ranked by how often they were hit, top two first because they are walls rather t
 3. **`break` is not implemented.** Declined deliberately rather than built — see below.
 4. **A `let` binding takes no type annotation**, so a fixed array is either a top-level `defvar` or a literal with
    every element spelled out. `(let [pts [4 rl/Vector2]] …)` parses as a two-element array literal and fails with
-   *unknown name rl/Vector2*. Cost: 32 hand-written `Vector2`s in one example.
-5. **Arithmetic is strictly binary** — *+ takes 2 arguments, given 5*.
-6. **No `sin`/`cos`/`abs` for floats.** The prelude has `sqrt-f32` and nothing else transcendental. Two `declare`
-   lines over libm, and `(max x (- 0.0 x))`; the examples each declare their own, which is a copy per file.
+   *unknown name rl/Vector2*. Cost: 32 hand-written `Vector2`s in one example. **Looked at and stopped — it is a
+   grammar question, not a missing feature.** Everything under the surface is already there: `Ast.binding` carries a
+   `bty`, `load.ml` renames through it, and `check.ml:723` consumes it as the `want` for the value. Only the way it
+   is written is open, and the parser says so where it refuses (`parse.ml:366`): `let` is a flat list of pairs, so it
+   cannot disambiguate by *count* the way `defvar` and `defconst` do — those read `[n t v]` as three arguments to a
+   form, and there is no such boundary between one pair and the next. Three surfaces, in the order they are worth
+   considering:
+   - **`(zeroed [4 rl/Vector2])` — `zeroed` takes its type as an argument.** Recommended. It is one extra branch in
+     the arity-0 `zeroed` case in `check.ml`, no parser change, no ambiguity, and it answers the actual complaint,
+     which is not "locals cannot be annotated" but "there is nothing here to infer *from*". It also reads as what it
+     does: the value is a zeroed thing of that type, not a name that has been told what it is.
+   - **A marker between the name and the type**, `(let [pts :- [4 rl/Vector2] …] …)` or similar. Unambiguous, and it
+     buys a general annotation rather than one form's escape hatch. The cost is a new piece of syntax in the binding
+     vector, which is the one place this language has kept looking exactly like Clojure's.
+   - **Bare `(let [pts [4 rl/Vector2] …])`.** The obvious spelling and the one that cannot work: `[4 rl/Vector2]` is
+     a well-formed two-element array literal, and telling the two apart needs types in the parser, which there are
+     none of by design.
+   Note that plan.org's rule is "annotate function signatures, infer locals", so the general annotation is a
+   deliberate absence and not an oversight — which is the other reason the `zeroed` route is the smaller answer.
+5. ~~**Arithmetic is strictly binary** — *+ takes 2 arguments, given 5*.~~ **Fixed.** `+ - * /`, `min`/`max` and
+   `bit-and`/`bit-or`/`bit-xor` fold left over two operands or more. `%` and the shifts stay at two, and one operand
+   is refused with the form to write instead — there is no unary minus and no reciprocal.
+6. ~~**No `sin`/`cos`/`abs` for floats.**~~ **Fixed.** `sin-f32` and `cos-f32` are `declare`s in the prelude now,
+   with the caveat written beside them: IEEE-754 makes `sqrt` correctly rounded and requires nothing of the kind for
+   `sinf`, so these are the one place in the prelude where native and wasm32 may disagree bit for bit. Float `abs` is
+   not wrapped, for the reason integer `abs` is not — it is `(max x (- 0.0 x))` over two builtins.
 
 **A `string` cannot be returned from C at all**, which is what makes `GetGamepadName` unbindable: *a string only
 crosses as a parameter — a C function that returns one returns something Flan has no owner for*. Same rule refuses