Destutter usage

Stream: general

[Alex Meiburg]

The docs for Destutter suggest

[2, 2, 3, 3, 2].destutter (≠)

as an example usage, but Lean 4 complains "unexpected token '≠'; expected ')', '↑', '↥', '⇑' or term". I'm guessing this is a Lean 3 vs Lean 4 issue. What's the right syntax, and should those docs be updated?

[Alex Meiburg]

Ah, apparently the new notation is (·≠·). Well, there's a lot of instances of (+), (<), etc. in the comments still in Mathlib :)

[Ruben Van de Velde]

Yeah, this is lean 3 syntax. Do you want to make a pull request?

[Daniel James]

There are a lot of instances of this.

> rg '\([+\-*/=≤<>≥≠⊆]\)' | wc -l
154

[Eric Wieser]

@Mario Carneiro had a proposal at one point to reintroduce this syntax, as it produces better terms than the dotted form

[Mario Carneiro]

My first choice proposal is to have the dotted form produce this output

[Mario Carneiro]

but alas lean4#2263 and lean4#2267 are both broken for complicated reasons that exceeded my patience