## 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):

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.

Last updated: May 09 2021 at 22:13 UTC