achlipala/frap

Notation suggestion for § 4.2 "A Stack Machine"

Closed this issue · 0 comments

Page 19 says "we write s1 ⋈ s2 for concatenation of two stacks s1 and s2." But notably, the next use of ⋈ is actually for concatenating instructions/programs.

There is a usage of ⋈ with stacks in Lemma 4.3 for the expression "⟦e⟧⋈s", but since (1) it's only pushing a single value onto the stack, and (2) it's the only apparent usage of ⋈ on stacks, it seems like it would be simpler to just stick to the already introduced ⊳ operator here, and instead introduce ⋈ as operating on programs.