leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: general

Topic: parsing with expected type


Yury G. Kudryashov (Dec 02 2019 at 06:12):

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

Simon Hudon (Dec 02 2019 at 06:30):

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


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll