[adeerkhan]

This is a prototype for proposal 3 of #1632 (a missing match case), in reply to the request to prototype 1–7. It is opened against bendlang/bend for review: bend2/bend.ts is human-written per AGENTS.md, so it is not a merge request as it stands. The branch is proto/1632-3-missing-match-case on the fork, 0d606f7b, rebased on main; the repo gate is green.
Changed the empty-match throw (bend.ts:3625). The message keeps the constructor's printed name; the Note names the constructor and the pattern to write: a nullary one by the way the surface spells it (0n for Zero, [] for Nil, True{} for True), a fielded one by its constructor alone — its fields may be dependent, so a case with them may not check — and a catch-all case for the rest. It names the pattern, not a whole case ...: line, because a match on several scrutinees takes one pattern each and the count is not known there.

On your repro:

SOME PROOFS FAIL
Error:
- message  : this match doesn't cover Zero
Location: pred
3 | def pred(n: Nat) -> Nat:
4>|   match n:
  |   ^^^^^^^^
5 |     case 1n+p:
Note: add a case for `Zero` (pattern `0n`), or a catch-all case.

15 existing tests with cases for … regenerate; tests/check/missing_nat_case.bend pins the Nat/0n spelling.