feat(language): an expression that only other files' terms fill is declared with expression: null, and prints as dots

[FBumann]

Prompt: I think an empty expression should be marked explicitly with expression: null

Prompt: It should probably be "..." in typesetting...?

Note

The following content was generated by AI.

What this changes

expression: null over a declared dims: defines an empty expression. Alone, the file reads it as it reads a given expression. merge fills it with terms, and a term now lands only on a definition. The typesetter prints the empty body as ….

Semantics, breaks, gate output, mutation table

Semantics (the two design answers from the conversation)

• Loaded alone, it is an open quantity, not 0. With 0, the constraint injection == 0 is refused ("neither side carries a variable"), so a balance fragment would not load on its own. The file reads the name as it reads a given expression: a quantity over the frame, of degree one, and a where does not read it. dims: is required. cases: and otherwise: are refused beside it.
• Terms land only on a definition, empty or written. A term still adds to a written body. A name that another fragment only reads under given:, or only uses in its math, no longer takes terms. The refusal names the rewrite (expression: null).
• Program. The name is under program.given.expressions, and GivenDeclaration.empty is set. Consumers need no new node, and the Expression union is unchanged.
• Printing. The definition prints as injection_{t,b} = \dots (Typst dots.h), through a new dots operator. The legend lists the name under Definitions, not Given. typeset_declaration prints its line.
• Advice. An empty expression draws no advice, because the null already says that other files fill it. This also keeps the golden model free of advice, so the model can carry the construct.
• Composed. The composed definition keeps the dims: its fragment wrote. This applies to a written body too: before this PR, _summed dropped the dims:. A merge that adds no term keeps the name empty.

Breaks (pre-1.0, no alias)

• Terms on a name that is only read or used are refused. test_a_term_lands_on_a_name_a_contributor_s_own_math_uses was deleted. Its case is now a refusal: test_terms_that_land_on_no_name_are_refused[terms-on-a-use-and-no-definition], next to [terms-on-a-reading-and-no-definition].
• The balance in docs/several-files.md and in declarations.md defines injection with expression: null, not under given:.
• The composed definition now also carries dims: when the definition has a written body (see above).

Docs

named.md has a new section, "An empty expression". The term rules changed in declarations.md and howto/compose.md. reading.md explains empty. The tutorial several-files.md now prints the …. The generated notation.md has a row for the new golden entry imports. The schema was regenerated (docstring only).

Gates

pixi could not be installed (network policy), so I ran each gate in a Python 3.12 venv:

• pytest -n auto: 2114 passed, with coverage and typst installed, so the line census and typst compile tests ran.
• ruff check, ruff format --check ., pyrefly check (0 errors), typos, and prettier --check on docs/. .all-contributorsrc fails prettier on main too.
• python -m tools.schema, python -m tests.typesetting.golden and python -m tools.notation were regenerated. I read their diffs.
• zensical build --strict shows one warning only: the docs.python.org inventory, which the proxy blocks. main gives the same warning.
• Not run: compile-tex (no tectonic), and the lefthook hooks as a whole.

Mutation table (hand-run, base ba21b23, git checkout -- restore, __pycache__ dropped, tree clean after)

Guard removed	Result
expression: null kept on write	caught: 7 failed, e.g. test_the_generated_page_is_current[notation]
expression: null needs dims:	caught: test_the_two_forms_do_not_mix[null-without-dims]
a null counts as an expression:	caught: 46 failed
a term lands only on a definition	caught: 5 failed
the sum keeps the definition's dims:	caught: test_the_sum_keeps_the_frame_of_its_definition
a reader is held to the empty frame	caught: test_a_reader_over_less_than_the_empty_definition_is_refused
an empty expression draws no advice	caught: 3 failed
the legend moves it out of Given	caught: 5 failed
typeset_declaration prints its line	caught: 5 failed

Not done

• An override patch cannot turn a written body into an empty one. A patch null drops the field, and the entry then has neither form.
• The bare form injection: null is refused by pydantic's generic message, because the entry needs dims:.
• specsolve does not read GivenDeclaration.empty yet. It sees the name as a given expression.

Why

See the prompts above.

🤖 Generated with Claude Code

https://claude.ai/code/session_01CQxVP5uX2V4rpvJNPhbyR2

---

Generated by Claude Code

[read-the-docs-community]

Documentation build overview

📚 mathspec | 🛠️ Build #34806241 | 📁 Comparing 645f053 against latest (8e4765a)

  🔍 Preview build  

9 files changed · ± 9 modified

± Modified

• changelog/index.html
• several-files/index.html
• howto/compose/index.html
• reference/api/index.html
• reference/notation/index.html
• reference/program/index.html
• reference/reading/index.html
• reference/language/declarations/index.html
• reference/language/named/index.html

[FBumann]

Prompt: Yes, do the change

Note

The following content was generated by AI.

This PR is closed in favour of #742, which implements the same feature. The explicit spelling moved there as a flag, empty: true, not as expression: null.

---

Generated by Claude Code