Where is func `String -> Syntax` used by syntax declaration?

Stream: lean4

[nrs]

I'm learning about Lean metaprogramming, and I was wondering whether there was a command I could call to get the inhabitant declaration for Syntax for a piece of Lean code. Alternatively, the actual function String -> Syntax that does this transformation would be super useful too!

[Mario Carneiro]

What function do you mean?

[Mario Carneiro]

Do you want to call the parser on a term or something?

[nrs]

Mario Carneiro said:

Do you want to call the parser on a term or something?

Yeah, for instance I want to get the Syntax inhabitant for fun n => n + n or def myNat : Nat := 2