Gabriel Ebner

> Syntax objects have arbitrary key-value maps associated with them, and one of the properties in that is the original, user-written syntax that eventually gave rise to the current object....

> ``syntax.node `have [(syntax.binder `h [A, P] [R])]`` Why does syntax.binder take A and P as arguments? (I'm concerned that we end up having two different syntax representations for before...

> David suggested the following idiom for transforming s : syntax. First, we expand and obtain e : expr := expand s. e subterms would contain references to s nodes....

> the binding structure is determined by the binding structure of the resulting core-language program, because the core-language program is the meaning of the expression. I think this is a...

I think I have an idea on how to deal with both queries 1-6 and the problem of renaming bound variables. We can add a "tracing" mode to the expander/elaborator,...

> It is also very useful to be able to single-step expansion Does this work well with the sets-of-scopes approach? If I see it correctly, you could have an eta...

> BTW, I read the paper "Binding as Sets of Scopes" (linked above), and I still don't understand why this approach is better than the locally nameless approach. I think...

> After I read your message, I started to question the feasibility of syntax -> syntax transformations. So the alternative is to expand everything directly into expressions, without being to...

> How do we know that the where is creating a scope? Let me explain where each of the scopes come from / what they mean: * 0: scope introduced...

Some idle thoughts: `syntax.node` should take a tag (of type nat) just like expr does now. Otherwise it becomes difficult to trace syntax object through the elaboration process. (Just think...