declId to ident / id

Stream: Is there code for X?

[Adam Topaz]

I am working with some TSyntax object of the form TSyntax `Lean.Parser.Command.declId. This has an identifier buried somewhere inside, plus potentially some universe annotations. Do we have a convenient way to extract the ident, or the identifier itself as a Name? If not, then what is the preferred way to obtain the identifier?

[Damiano Testa]

does id[0].getId work for you?

[Damiano Testa]

id[0] should be the "plain" identifier.

[Adam Topaz]

is there a getElem instance for TSyntax?

[Damiano Testa]

Oh, possibly laundering it through .raw?

[Adam Topaz]

But then I can't use getId

[Damiano Testa]

So, id.raw[0].getId.

[Adam Topaz]

Oh that does work! Thanks!

[Damiano Testa]

I think that it might work, just give "unexpected behaviour" if you give a non-ident.

[Adam Topaz]

Thanks! You are a syntax guru!

[Damiano Testa]

I'll take the compliment, but still am skeptical... :smile: