request for help with filter notation

Stream: mathlib4

[Scott Morrison]

lean4#2790 changes the way some "internal" errors are handled, and it particular makes it "harder to catch" them, so when they occur they will break whatever is going on.

#8056 is the Mathlib adaptation PR.

The main problem in Mathlib itself is that the 𝓝[≠] notation is broken, with many usages now resulting in a "max recursion depth" error (that was previously being caught and recovered from).

If anyone is available to look at this (someone interested in both filters and notation? :-), that would be very helpful.

[Patrick Massot]

@Scott Morrison I hope I fixed this one. It took me a lot more time to locate the workaround commits I should revert than to see why this notation was problematic. I think it would have been faster to ask before writing the workarounds (but I'm fully aware that you need to be efficient when doing this huge and very useful work of porting Mathlib to recent changes in core).

[Jireh Loreaux]

@Patrick Massot do you mind explaining what was wrong with the notation? I looked last night and couldn't figure out the problem.

[Patrick Massot]

It uses {x} which very often requires type ascription help.

[Scott Morrison]

@Patrick Massot, sorry, I'm unclear what state this is in now. Should I revert the workarounds I made?

[Patrick Massot]

The filter stuff should be good, I reverted your commits.

[Scott Morrison]

@Patrick Massot, would you mind checking again? When I look at the PR diff it still seems to have many nbhdsWithin.

[Patrick Massot]

Sorry, it seems my heuristic to figure out which commit to revert was not good enough.

[Patrick Massot]

I'll take another look.

[Patrick Massot]

@Scott Morrison it should be ok now.