Parse TLA+ set union and intersection operators

[GTrunSec]

Summary

• Parse the standard TLA+ set operators \cup and \cap, including \union and \intersect spellings.
• Place them at the same left-associative precedence between comparisons and ranges, matching the TLA+ operator table.
• Add accepted roundtrip cases for all four spellings and a rejected missing-operand case.

Verification

• gerbil compile -S languages/tla-plus/v1/grammar.ss languages/tla-plus/v1/parser.ss languages/tla-plus/v1/parser-test.ss
• gerbil test -v 3 languages/tla-plus/v1/parser-test.ss (MODULE-OK, HARNESS-OK, OK)

This change covers native syntax. TLC model checking remains a separate qualification step.

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-09-27T16:13:45.129149Z	ed10b6a	PR opened

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[GTrunSec]

Consolidated into PR #13 at 80fef34. The TLA+ set-operator patch has the same stable patch ID as ed10b6a, and its native parser test passes on the combined branch. Keeping #13 as the sole open PR for this parser work.