setOf unexpander

Stream: mathlib4

[Dan Velleman]

I think there is a small bug in Mathlib/Init/Set.lean. The unexpander for setOf includes this line:

  | `($_ fun $x:ident : $ty:term ↦ $p) => `({ $x:ident : $ty:term | $p })

I believe it should be

  | `($_ fun ($x:ident : $ty:term) ↦ $p) => `({ $x:ident : $ty:term | $p })

The delaborator puts parentheses around $x:ident : $ty:term, so the unexpander has to look for those parentheses. Note that this will only cause a problem when using the option pp.funBinderTypes; without that option, the delaborator leaves out the type, so this line of the unexpander doesn't get used.
If others agree, I will file an issue.

[Dan Velleman]

Also: I notice that in many unexpanders, the syntax starts with $(_) rather than $_. Can someone explain what the difference is?

[Sebastian Ullrich]

The second syntax is newer

[Dan Velleman]

So both are acceptable, and they mean the same thing?

[Dan Velleman]

Thanks Sebastian. Do you agree about the minor bug in the unexpander?

[Dan Velleman]

It looks like the same problem appears (twice) in Mathlib/Order/CompleteLattice.lean

[Sebastian Ullrich]

Yeah, sounds sensible