intellij-arend icon indicating copy to clipboard operation
intellij-arend copied to clipboard

New inspection: report name shadowing in data constructors

Open marat-rkh opened this issue 3 years ago • 0 comments

Screen Shot 2022-02-21 at 11 06 56 AM

Here at line 724 I have accidentally introduced {B : Type} which shadows B in the pattern on the left side of =>. This lead to strange issues with implicit arguments inference, I spent quite some time trying to figure out what is wrong. It would be nice if IDE reported name shadowing in this case.

marat-rkh avatar Feb 21 '22 08:02 marat-rkh