Using lambda

Stream: lean4

[Nir Paz]

This has probably been brough up somewhere, but are there any plans to ever un-keyword λ? Obviously it's pretty extreme non-backwards compatibility, but it would be really nice to reclaim λ.

[Nir Paz]

Was there any discussion of this in the early days of lean 4? That would have been the time to pull the trigger.

[Julian Berman]

Not since 4 weeks ago :D -- #mathlib4 > lambda

[Etienne Marion]

This was recently discussed here.