Stream: metaprogramming / tactics
Topic: parser documentation
Patrick Massot (Jan 21 2021 at 22:22):
Is there any to avoid the horrible error message on hover when using a custom parser? I have defined tactics whose only argument is a complicated custom parser and every time my mouse gets over an application of such a tactic I have half a page of error message complaining Lean wasn't able to synthesize a description for this parser.
Patrick Massot (Jan 21 2021 at 22:26):
I should have thought more before posting. I realized
rcases certainly hasn't an auto-generated parser description and I see a promising
with_desc there. I'll investigate.
Bryan Gin-ge Chen (Jan 21 2021 at 22:26):
I'd be interested in finding out how to fix this for the tactics which currently suffer from this.
Patrick Massot (Jan 22 2021 at 10:43):
Bryan, which tactic are you talking about? I think there is no problem using
with_desc to fix everything.
Bryan Gin-ge Chen (Jan 22 2021 at 15:14):
ext1 seem to be broken at the moment:
import tactic example (s t : set ℕ) (h : ∀ x, x∈s ↔ x∈t) : s = t:= begin ext1 x, -- ^ hover here end
I'll take a look at how
rcases does things too.
Last updated: May 09 2021 at 22:13 UTC