Aside: Explicit rule for `let` in MixML
In MixML $\mathtt{let}$ binding of one module inside another is defined as syntactic sugar:
This definition highlights the minimalism of MixML (along with other definitions): one can express the entire ML module system in it. Unfortunately, the compactness of the language can hinder one’s understanding of these “macro-expressible” constructs. For my own benefit I wrote out the explicit elaboration rule for $\mathtt{let}$, so why not post it here:
