parser documentation

Stream: metaprogramming / tactics

[Patrick Massot]

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]

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]

I'd be interested in finding out how to fix this for the tactics which currently suffer from this.

[Patrick Massot]

Bryan, which tactic are you talking about? I think there is no problem using with_desc to fix everything.

[Bryan Gin-ge Chen]

For example, ext and 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.