Quoting a TSepArray

Stream: Is there code for X?

[Jeremy Salwen]

How do you explicitly construct a value of type TSepArray using quotation?

For example

quote (#[`simp, `foo])

gives a TSyntax, not a TSepArray.

[Kyle Miller]

Could you give more context (maybe a #mwe)? The quote function is for creating syntax that would evaluate to #[`simp, `foo]. Is that what you want? Or are you wanting a TSepArray `ident to splice in somewhere?

[Jeremy Salwen]

I want to call a library function that takes TSepArray (addRelatedDecl), and I just want to construct the argument explicitly.

[Jeremy Salwen]

Constructing a TSyntax seemed close to my goal of constructing a TSepArray, but maybe that is the wrong path.

[Kyle Miller]

One thing you need to make sure to do is create a TSyntax `Lean.Parser.Term.attrInstance for each attribute, which isn't just a Name, so that takes a bit more work. quote is specifically for creating a TSyntax `term (a.k.a. a Term).

[Kyle Miller]

Do you need this to be programmatic, or will it be a fixed array?

[Jeremy Salwen]

It is just a fixed array.

[Kyle Miller]

I guess this is one way to do it:

example : MetaM (Syntax.TSepArray `Lean.Parser.Term.attrInstance ",") := do
  let arr : Syntax.TSepArray `Lean.Parser.Term.attrInstance "," := ∅
  let arr := arr.push (← `(Lean.Parser.Term.attrInstance|simp))
  let arr := arr.push (← `(Lean.Parser.Term.attrInstance|foo))
  return arr

[Jeremy Salwen]

Ah, thank you!