Syntax from object

Stream: lean4

[Marcus Rossel]

What is the idiomatic approach to creating the Syntax object for some given object?
E.g. I have a simple Pos type, and right now I convert it to syntax as:

structure Pos where
  x : Int
  y : Int

def Pos.toSyntax (p : Pos) : Syntax :=
  Syntax.mkCApp `Pos.mk #[Syntax.mkNumLit s!"{p.x}", Syntax.mkNumLit s!"{p.y}"]

But if e.g. I'd have to create a Syntax object for a List Pos I'd already struggle with that.
I guess I could express it as nested applications of List.insert with all the elements in the list, but that feels unnecessarily cumbersome to me - so I'm not sure if I understand how to construct Syntax objects correctly/idiomatically.

[Gabriel Ebner]

That's easy. You first declare a Quote Pos instance using your Pos.toSyntax function.

[Gabriel Ebner]

(Which should probably be written as Unhygienic.run `(Pos.mk $(quote p.x) $(quote p.y)) )

[Gabriel Ebner]

And then you automatically get a quote : List Pos → Syntax function because we have a [Quote α] → Quote (List α) instance.