[Agda] How can I implement naive sized lambdas?

[Georgi Lyubenov]

Thanks for the responses!

In the end I went with using sizes as demonstrated by gallais - after
avoiding SIZEMAX using SIZEINF I had no more issues. The result can be seen
here <https://github.com/googleson78/lcpt-1920/blob/master/agda/Lambda.agda>
.

On Wed, Mar 25, 2020 at 12:10 PM Guillaume Allais <
guillaume.allais at ens-lyon.org> wrote:

> Hi Georgi,
>
> I would advise against working directly with raw names: you get
> absolutely no support from the typechecker to enforce well-scopedness
> and it is very easy to shoot one's foot off.
>

I am aware, but my initial goal itself is to implement named and nameless
lambdas, implement and prove conversion between the two representations (+
other stuff eventually, like beta reduction).
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.

Thanks for the hint and snippet(s) on parallel substitution - this is the
first time I've seen the approach and will definitely need to check it out!

=======
Georgi
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200404/a8b410d9/attachment.html>