Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: parser documentation


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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, xs  xt) : 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