Long tut alpha equivalence

[haroldcarr]

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.

[wilbowma]

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.

[haroldcarr]

If =α is defined for Lambda/n then sd has to be defined for Lambda/n too.

[wilbowma]

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.

[mfelleisen]

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.

[haroldcarr]

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.