Inferring the type of syntax during term elaboration

Stream: lean4

[Thomas Murrills]

While writing a term elaborator, let's say I have to match on syntax of the form $xs,* where the xs are terms. How do I infer the types of these xs in context? Do I need to run elabTerm on them first (somehow), then use Lean.Meta.inferType on the resulting Expr's? Or is there a special way to do this within TermElab somehow?

[Gabriel Ebner]

If you match on $xs,*, then you will get an xs : TSepArray `term ",". This is still Syntax, so you will indeed need to elaborate it first.

[Gabriel Ebner]

Ideally, you should only run elabTerm once on every syntax object. That's why there is no elabTerm+inferType combo.

[Thomas Murrills]

Right—I was indeed worried about elaborating more than once. That said, I do need the types...hmmm. I wonder what the best way to proceed is.

Would I risk throwing away important information that might be used to infer the types if I simply, say, turned TSepArray into an Array Syntax somehow and mapped elabTerm · none over it, then inferred the types from those expressions? (Would that even be the right way to do it?)

[Thomas Murrills]

Or is there a way to "elaborate in place" somehow, by, I suppose...re-inserting elaborated expressions into syntax with a note that they've been elaborated and don't need to be elaborated further below that node? (It seems like the ladder of abstraction only goes up, from Syntax to Expr, so I'm guessing maybe not, but worth a shot...)