[Agda] How can I implement naive sized lambdas?

[Sandro Stucki]

Hi Georgi,

> That said, is there some "well-scoped syntaxes 101" resource that I could read? The only particular thing I am aware of is "Everybody's Got To Be Somewhere" by Conor McBride.

There is some support for well-scoped parallel substitutions in the
Agda standard library, along with an example of how to use it for the
untyped lambda calculus:

  https://github.com/agda/agda-stdlib/blob/master/src/Data/Fin/Substitution.agda
  https://github.com/agda/agda-stdlib/blob/master/src/Data/Fin/Substitution/Example.agda

Not sure this qualifies as a 101 though. For what it's worth, it
illustrates the use of parallel substitutions as suggested by Andreas,
and people seem to find it useful for their projects.

/Sandro