<div dir="ltr"><div dir="ltr"><div>Thanks for the responses!</div><br>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 <a href="https://github.com/googleson78/lcpt-1920/blob/master/agda/Lambda.agda" target="_blank">here</a>.<br><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Mar 25, 2020 at 12:10 PM Guillaume Allais <<a href="mailto:guillaume.allais@ens-lyon.org" target="_blank">guillaume.allais@ens-lyon.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi Georgi,<br>
<br>
I would advise against working directly with raw names: you get<br>
absolutely no support from the typechecker to enforce well-scopedness<br>
and it is very easy to shoot one's foot off.<br></blockquote><div><br>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).<br>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.<br><br></div></div></div>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!<br><br>=======<br>Georgi</div>