TSyntax `num from a `Nat`?

Stream: lean4

[Scott Morrison]

How do I get a TSyntax `num from a Nat?

[Scott Morrison]

Ah, found my own post with an answer, although it seems a bit round-about.

[Scott Morrison]

let n : TSyntax `num := Syntax.mkNumLit <| toString n

[Kyle Miller]

I think the most straightfoward way is let n : TSyntax `num := quote n

[Kyle Miller]

This is doing exactly the same thing (the instance is instance : Quote Nat numLitKind := ⟨fun n => Syntax.mkNumLit <| toString n⟩), but the quote interface is nicer