Leonardo de Moura

@jroesch Should we close this one? I recall that @david-christiansen suggested this is not a good idea when he visited us, and it will "backfire", but I don't remember the...

The compilation strategy based on the primitive recursor `rec` is also useful when handling reflexive types. See #1620

> In Lean, (elaborated) expressions have a tag field (an unsigned integer). I guess we could keep a map/array of syntax trees after elaboration, and have the tags index into...

> @david-christiansen Is there anything better in the literature? Skimming through the papers that Leo posted, nobody even seems to mention infix operators. @gebner David sent me the following additional...

> But that makes modifying (and then pretty-printing) syntax objects awkward. Ideally you could transform syntax trees by just traversing the tree. Say you want to rename a constant c...

@kha How do we feel about this change?

> I think we also need an expand_command : syntax -> tactic environment. @gebner I missed this one. I agree with you. However, I think we will also need `expand...

I'm considering the following approach: 1- `reader` produces a `syntax` object similar to the one described by @gebner above. The binding sites are not resolved. So, it is easy to...

> We could put them into the syntax.node part instead (just like before name-resolution): > > syntax.node `have [A,P, syntax.binder `h R] Great. > Extra name-resolution step: Seems like a...

@david-christiansen Thanks for the feedback. Your design makes sense. My concern is that it doesn't support operations such as `expand_macros : syntax -> syntax`. That is, we would only be...