racket
Long tut alpha equivalence
Language Lambda/n is defined and used in a test, but the =a(lpha) function is defined in terms of language SD and uses the sd metafunction that is also defined on SD.
It looks as if the intended behavior is for the test to remain as is, but that =α be defined for Lambda/n instead of SD so the test makes sense.
If =α is defined for Lambda/n then sd has to be defined for Lambda/n too.
Looking carefully, there are clearly some issues with the declared languages in this section. sd/a and sd look as if they should be defined for Lambda, based on their tests. If they didn't have contracts, none of this would be a problem---redex is happy to ignore language declarations a lot of the time. We could use define-extended-metafunction to update the languages and contracts, but that hasn't been introduced in the tutorial.
FWIW, the tutorial consists of notes from the 2015 Redex workshop. The lecture notes supported live demos and worked at the time. The problem sets were derived from working solutions.
I guess when we migrated these notes into our docs, things got shuffled in ways that leaves copy-and-paste readers perplexed.
What you need to state first is a guideline for what you want to achieve, what kind of reader you want to support.
Do you want readers to chase the definitions need to explore a particular point in the notes? Text books take this approach, partly because the chasing can serve a pedagogic role.
Do you want easily flowing test? Do you want to support it with margin notes that link to complete files?
Do you want text interrupted by ever-growing programs? People already find scribble’s format heavy because so little content fits into large vertical space.
Don’t just fix local problems randomly.
The tutorial gives the impression that run can run it at any point, up to the point one is reading. To me, that is useful.
For now, I will just keep sending "random" pull requests that "fix" things I run into.