Make Interleave agree with the rest of the module on the empty sequence

[lemmy]

Interleave was the only operator that turned an empty argument into a non-empty result. It now yields the identity, as Zip, FlattenSeq and Reverse already do.

This is a breaking change, but a narrow one: it is confined to a single input, no other operator in the module reaches that input, and no proof depends on it.

[Refactor]

[Copilot]

🟢 Approval recommended

The implementation matches the existing documented behavior and is adequately covered by focused tests.

Pull request overview

Aligns Interleave’s empty-sequence behavior with its documented contract and related sequence operators.

Changes:

• Returns <<>> when both inputs are empty.
• Adds bounded property tests covering length and ordering invariants.

File summaries

File	Description
modules/SequencesExt.tla	Corrects the empty-input result and documents the rationale.
tests/SequencesExtTests.tla	Updates the empty-case expectation and adds invariant coverage.

Review details

• Files reviewed: 2/2 changed files
• Comments generated: 0
• Review effort level: Balanced

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[muenchnerkindl]

This definition clearly makes more sense than the previous one. Assuming Len(s) = Len(t), the operator now satisfies the recursive equation

Interleave(s,t) = IF Len(s) = 0 THEN << >> 
                  ELSE << <<Head(s)>>, <<Head(t)>> >> \o Interleave(Tail(s), Tail(t))