Discussion for v4.14.0 and v4.15.0-rc1

Stream: general

[Filippo A. E. Nuccio]

Thanks @Kyle Miller for 5528, I have long been hoping to see this.

[Jireh Loreaux]

@Kyle Miller Regarding lean4#5528, Junyan just posted there the same confusion I had upon reading your comment:

Dot notation doesn't work when x is a function, so (@x).f isn't useful as an interpretation.

Yes, it does?

import Mathlib.Logic.Function.Defs
variable {α β} (f : α → β)
#check f.Injective

[Jireh Loreaux]

(discussion thread for #announce > v4.14.0 and v4.15.0-rc1)

[Floris van Doorn]

I agree with the sentiment of Kyle's point though. Implicit arguments are (almost) exclusively used for dependent arguments, and declarations in the Function namespace are almost exclusively used for nondependent functions, so the (@x).foo is rarely useful.

[Notification Bot]

2 messages were moved here from #announce > v4.14.0 and v4.15.0-rc1 by Floris van Doorn.

[Kyle Miller]

Yeah, that's what I was thinking about @Floris van Doorn. I meant "doesn't work" as in "dot notation for functions is generally broken". docs#Function.swap is an example that fails (lean4#1629).

[Kim Morrison]

Just a heads up that v4.15.0 and v4.16.0-rc1 will be slightly delayed by our holiday schedules, don't expect these until about Jan 5.