[nicolas-abril]

A second simplification pass over safe.ts, with the same output. It makes room for #1896 under safe.ts's 24000-token cap. safe.ts goes from 23289 to 22875 ttok. #1896's η commits, picked onto this branch, apply cleanly and land at 23952.

What

Helpers:

• lams2(q, l, b) builds λt => λf => b at q, a default arm's binders. swi's empty default wrote these λs out by hand; now both of swi's cases build them. The default arm passes copies(e, q, b, [l, l + 1]) as q. It replaces pair_lams.
• uses had one caller left, tree's rebuild check, which now reads o_uses itself.
• spec_val had one caller, args, and is inlined.
• The out-of-scope fixed point in safe_pass finds each def's names the first time it asks, then reuses them, instead of walking the def again on every pass. As before, it walks nothing when no def is out of scope.
• safe_book and safe_pass share an Out type.

Shorter forms:

• term's ∀ case builds its node in one literal, A before B as before. Switch cases keep their braces.
• let_term, rwt_term and adt_emit use their one-use locals in place, in the same order.
• tele_open's return type is inferred from the record it builds.
• adt_emit applies D.arms to the tag with apps, as everywhere else.
• def_emit's no-model reason goes straight into ?? oos(..), which builds it only when no model is found; the else branch it covers is parenthesized. Its type goes into e.out without a local.
• kernel_bin reads $BENDTT directly, and its comment names LEAN_VERSION instead of repeating it.

Comments:

• As in bend.ts and comp.ts, which comment 3% and 5% of their functions, a comment that only restates its code goes. That covers 19 one-liners, including those over vr, tkey, node, fill, wnf, all_of, ctr_term, o_refs, apps and alls. Comments that give a reason, a contract or an encoding stay, or move into the code:
  • mentions takes a B.LTerm, so passing an unlowered term (whose binders hide their variables in closures) is a type error;
  • no_ctr is no_ctr_left: every constructor matched away, not a datatype declared with none;
  • mats says h runs from the last label to the first, and that what h names goes out in that order.
• safe_book's comment points to the header for the out-of-scope rule instead of repeating it; kind's and run_read's say the same in fewer words.

Checks

• -o on all 1795 files of tests/, main (0a41eea) against this branch: the same BendTT and the same messages on every file.
• bunx tsc -p bend2/pack: no errors in safe.ts.
• bun gates/_run.ts: repo 54 / 54, test 1782 / 1782, perf 124 / 124, ping 80 / 81 (pass).
• bun gates/safe.ts tests: the same verdict as main on every file: agree 1143, unsafe 142, bend2 rejects 507, out of scope 3, false reject 0, timeout 0, infrastructure 0.

🤖 Generated with Claude Code