Where should mkTuple go

Stream: Is there code for X?

[Joachim Breitner]

This question is dual to the usual one on this channel: I have a function, but I need the right place for it.
Which Lean module is the natural home for this function:

/--
Create Tuple syntax (`()` if the array is empty, and just the value if its a singleton)
-/
def mkTupleSyntax : Array Term → MetaM Term
  | #[]  => `(())
  | #[e] => return e
  | es   => `(($(es[0]!), $(es[1:]),*))

[Scott Morrison]

If Std.Lean.Syntax had already existed, I would say there. Possibly still there.

[Joachim Breitner]

I need it in core, though

[Scott Morrison]

Right next to src#Lean.Elab.Term.mkPairs?

[Scott Morrison]

Maybe just right at the point you need it, until there is evidence it warrants going somewhere higher.

[Joachim Breitner]

Somehow I recall someone saying “ah, that (mkPairs)’s defined before we have quotations”. But yes, if I can use `(…) there then that’s natural. I should just try :-)

[Mario Carneiro]

you can use quotations anywhere, although for quotations in Init you can't use syntax that hasn't been defined yet