Ahhh, my bad. I thought you were the same commenter as the first guy, and I doubly goofed by misreading the comment in the first place. The dangers of commenting before coffee. You're right, the difference between redex models and racket's implementation of them would be confusing, and I don't have enough direct knowledge to provide any insight there.