Comment by JoelMcCracken

ah nice explanation. I've actually read (or tried to) the "macros as a set of scopes" paper that IIUC lean 4's scoping is based upon; I did watch the talk on lean4's macro system. Does it not have some kind of "set of scopes" tracking?