underscores are holes

Stream: general

[Johan Commelin]

I really love the new "_ is a hole" feature!
Thanks @Gabriel Ebner

[Reid Barton]

What is this? Weren't underscores already holes?

[Patrick Massot]

Holes in the sense of hole commands I think.

[Pedro Minicz]

Could you please elaborate? I'd be very interested in knowing what exactly changed.

[Mario Carneiro]

Previously, you could type {! !} where a term is expected, and you get a lightbulb with suggestions a.k.a "hole commands"

[Mario Carneiro]

Now the same thing happens on any _

[Utensil Song]

See https://leanprover-community.github.io/mathlib_docs/hole_commands.html for more info (BTW, it's not updated to reflect this change yet)

[Bryan Gin-ge Chen]

Thanks for pointing that out. I just made a PR: doc-gen#29

[Bryan Gin-ge Chen]

Pedro Minicz said:

Could you please elaborate? I'd be very interested in knowing what exactly changed.

The specific change is at lean#307, if you feel like digging into the C++...