feat(language): a cased expression writes its fallback as otherwise, outside the cases

[FabianHofmann]

Prompt: "start the otherwise implementation"

Implements the change I asked for on #168. Stacked on feat/cases-proved-apart.

Note

The following content was generated by AI.

The value wherever no when holds moves out of cases: and becomes the block's own otherwise:. No name inside cases: is reserved, and the cases carry no order — so a file a key-sorting formatter produced says what it said before.

expressions:
  previous_status:
    foreach: [snapshot, generator]
    cases:
      always_on: { when: "not committable", expression: 1 }
      boundary:  { when: "committable and position(snapshot) == 0", expression: status_initial }
    otherwise: shift(status, over=snapshot, offset=1)

_default_is_the_last_case is deleted, and with it the five hand-written errors that policed a reserved name inside a map of user-chosen ones:

retired	now
"needs a case named default"	a `cases:` block needs an `otherwise:`
"default is written last"	deleted — nothing depends on order
"only case is default"	min_length=1 on cases:, published in the schema
"default carries a when:"	structurally impossible
"opening carry no when:"	the missing-field error on a required when:

One message the table did not have: otherwise: written without cases:, the mirror of the missing one, which no schema constraint catches.

The three golden .out files do not change. The rendered maths is identical, which is the check that this is input-only.

What was not just a spelling change

dimensions.py never checked the fallback's dims. With default inside cases: it came along in the loop for free; outside, it would have escaped, and a value carrying a dim the frame lacks would have reached lowering. The frame check now runs over the cases' values and otherwise, so otherwise: load under foreach: [generator] is still a DimensionError. test_a_case_may_not_widen_the_frame moved onto the new spelling and fails without the fix.

validation.py likewise now checks the otherwise body for unknown names, comparisons and the ceiling.

Everything downstream of the parse is untouched. expansion._parse_cased appends the fallback as the last CaseArm with when=None, so CasesNode, resolution, lowering, walk.py — which already found the fallback by arm.when is None rather than by name or position — the dim algebra and boundedness see exactly what they saw before.

Checks

pixi run ci clean: lint, 877 passed, mkdocs build --strict, 27 TeX documents compiled.

877 against the base branch's 880: the five default-shape parametrized cases are replaced by two form cases (no-otherwise, otherwise-alone) and two shape tests (..._says_where_it_applies, ..._carries_at_least_one_case).

Not done here: the base PR's body still describes the default design. It wants rewriting rather than appending to, and that belongs on #168 once this lands.

[read-the-docs-community]

Documentation build overview

📚 math-spec | 🛠️ Build #34298182 | 📁 Comparing b2cd7aa against latest (a9237ec)

  🔍 Preview build  

16 files changed · + 2 added · ± 14 modified

+ Added

• examples/commitment/index.html
• reference/math_spec/exclusivity/index.html

± Modified

• examples/index.html
• reference/notation/index.html
• reference/language/expressions/index.html
• reference/math_spec/dimensions/index.html
• reference/math_spec/expression_parser/index.html
• reference/math_spec/model/index.html
• reference/math_spec/program/index.html
• reference/math_spec/validation/index.html
• reference/math_spec/typesetting/format/index.html
• reference/math_spec/typesetting/latex/index.html
• and 4 more...

[FBumann]

Good reasons!
Didn't look at the code yet
Why otherwise? Did you check what proper math calls this?

[FabianHofmann]

math calls it otherwise ( \begin{cases} conventionally ends & \text{otherwise}). so this it says what is actually means to say. default would work too, but otherwise gives the clear indication that we are talking about the cases where not when hits.