I’m taking a look at the redex semantics for r6rs, and I’m confused; I can’t find ‘define’. Well, actually, the whole module system seems to be missing. If I want to use this semantics as the basis for some kind of reasoning over programs that use define, am I required to rewrite them as a top-level letrec? Asking for a friend.

I think it’s just a semantics of expressions

Hmm, that’s a bit disappointing. I have a student who’s trying to prove correctness of an early pass of Chez. Okay, we’ll just make it up :slightly_smiling_face:.