parsing with expected type

Stream: general

[Yury G. Kudryashov]

Hi, how do I parse input providing an expected type? I want to allow ⟨_, _⟩ as an argument to a custom command.

[Simon Hudon]

Use texpr to parse it and, with e the resulting pexpr, elaborate the expression using to_expr ``(%%e : %%my_type)