feat(language): a file adds a term to an expression another file defines, under given:

[FBumann]

Prompt: "Try it. As a stacked PR" — then: "Yes. The rule is that a fragment that declares its expressions adds to an existing one, must find that existing one. And if multiple fragments define such an addition, a REAL expression with that name still needs to be found somewere"

Note

The following content was generated by AI.

term: on a given: expressions: entry is what a file adds to a name another file has. merge defines the name as the definition one fragment writes, if any, plus every term, and refuses terms that land on a name no fragment defines, reads or uses. The additive flag, the kept entry and the load-time exemptions are gone.

Stacked on #732, and replaces its sum design.

The rule

merge writes nothing a fragment did not write, except a +. It joins two fragments' text in two places: the objective, and a named expression that terms add to. Every other block is copied as written, refused where two fragments own it, or held identical where it is a dimension or a relation. A given: entry is checked and discharged, never altered. Merge fills a reading or extends a definition, and never invents a name.

# generators.yaml adds to a sum another file reads
given:
  expressions:
    injection:
      dims: [snapshot, bus]
      term: sum(dispatch, by=gen_bus, over=generator, into=bus)

# network.yaml reads it, and says nothing about sums
given:
  expressions:
    injection: { dims: [snapshot, bus], description: what the components put into a bus }
constraints:
  balance: { dims: [snapshot, bus], expression: injection == 0 }

Roles

Role	Writes for the name	Alone, the name is
definer	a body under expressions:	its body
reader	a given: entry with dims	a column somebody provides
contributor	a given: entry with dims and term	the same column, the whole sum

A fragment plays one role per name. A definer's meaning changes when composed, as a fragment's objective does, and no mark is asked for on either.

What this changes

• given: expressions: takes term, one expression, and no longer takes additive. A file that only reads the name writes no term.
• Alone, a contributor reads the name as the whole sum, composed or not, so one file means one thing. A term is resolved in its own file, at load: it may not read the name it adds to, may not carry a dimension the entry does not state, and is held to degree two.
• merge defines a name some fragment adds a term to as the definition one fragment writes under expressions:, if any, plus every term, each in parentheses, in fragment-name order. Nothing declares that a name is a sum. A later merge adds to the composed definition the same way, so no entry is kept. A definition written as cases: is refused. Two definitions still collide, and the message names term:.
• A term has to land. Terms on a name no fragment defines, reads without a term, or uses in its math are refused, with the near miss named. That is what a mistyped target looks like.
• The description. The definition keeps its own, or takes the first a reader wrote. A term carries none.
• override edits a term like any field of a given entry, and term: null makes the entry a plain reading.
• Typesetting. The legend's Given line says "an expression this file adds a term to". The term prints under Definitions as injection = ⋯ + term, a negated term as a subtraction, and typeset_declaration prints that line. ellipsis joins the operator vocabulary, so the golden model gains a term and docs/reference/notation.md a Given section.
• Advice for a term says merge() sums it with what the other files declare.
• Program. ExpressionDeclaration is untouched. GivenDeclaration.term holds the resolved term. program.given still means what a host must provide.
• Docs. The language reference section is now "A term a file adds"; the tutorial's component files carry terms, and its "Leave the network out" step shows the landing refusal; the how-to table and reading.md follow.

Why

The reader-side flag leaked into a regular declaration, made a hub file mean one thing alone and another composed, and needed a kept entry so a second merge could add. Marking the contributor removes all three: a term is a fact about the file that writes it, decidable there. Consent from the definer was considered and dropped: the objective is already extended by any fragment without a mark, and the one thing a mark would catch, a term that lands nowhere, the landing rule catches.

Method, guards, gates, what was not done

Guards, each with the test that fails without it (tests/test_terms.py). At load, test_what_a_term_may_not_be_is_refused_at_load: a term wider than its entry, a term reading the name it adds to, a term that does not load, a term of degree three, a term beside a definition of the name. At merge: terms that land nowhere and a mistyped name (test_terms_that_land_on_no_name_are_refused), a cased definition a term adds to, two definitions, readers disagreeing on the frame, a definition over a dimension the readers do not state.

Coverage moved. tests/test_additive.py is tests/test_terms.py. The old marked-hub and contributor-reads refusals have no counterpart because the cases no longer exist. test_several_files_page.py runs six Python blocks now: the tutorial prints a contributor's math alone.

Gates. Pixi cannot be installed in this container. In a Python 3.12 uv virtualenv with the runtime pins of pixi.toml:

pytest tests -n 8                         2062 passed, 27 skipped
ruff check . / ruff format --check .      clean (ruff 0.16.9)
pyrefly check                             0 errors (9 suppressed)
prettier --check docs CHANGELOG.md        clean
python -m tools.schema                    regenerated, committed
python -m tools.notation                  regenerated, committed
python -m tests.typesetting.golden        regenerated, committed
python -m tools.gallery --check           13 page(s) current

Not run: docs-build, compile-tex, typos, reuse lint, zizmor, taplo. The twenty skips beyond #732's count are the docs-feature tests in tests/test_docs.py, which the bare environment skips.

Not done.

• A second combinator. A product would be a second field beside term:, with one rule: one name, one combinator across the fragments. Nothing here needs it.
• A patch that appends to a sum. override replaces a term and never adds one; a project that wants to add writes a fragment and merges it. If a caller ever needs add: on a patch, it is the summed-not-overwritten rule inside override, a PR of its own.
• The first description among readers is taken in the order the fragments are passed, as _agreed already does for a shared dimension in feat(language): a spec is composed from files that each state part of it, and patched with files that each change part of it #732.
• A term is one expression string. A cased contribution is named as its own expression and added by name, which the schema now says instead of a check.

🤖 Generated with Claude Code

https://claude.ai/code/session_01H1F2gprjeiGPnvDaWjZwBB

[read-the-docs-community]

Documentation build overview

📚 mathspec | 🛠️ Build #34764513 | 📁 Comparing d587b52 against latest (0efbf59)

  🔍 Preview build  

21 files changed · + 8 added · ± 13 modified

+ Added

• several-files/index.html
• examples/library/index.html
• howto/compare/index.html
• howto/compose/index.html
• examples/library/composed/index.html
• examples/library/generator/index.html
• examples/library/load/index.html
• examples/library/surface/index.html

± Modified

• index.html
• changelog/index.html
• examples/index.html
• about/limits/index.html
• reference/api/index.html
• reference/glossary/index.html
• reference/language/index.html
• reference/notation/index.html
• reference/program/index.html
• reference/reading/index.html
• and 3 more...

[FBumann]

Prompt: "You build it / Fold it into 732 / Close 734"

Note

The following content was generated by AI.

Superseded by #732. This PR's commits were fast-forwarded onto feat/composition (to d587b52). #732 then makes a term: name an expression of its own file, and adds each term to the sum by name.

---

Generated by Claude Code

---

Generated by Claude Code