Curiosity about curly brackets

Stream: new members

[Pedro Minicz]

Curly brackets are used to indicate implicit arguments, but some definitions on mathlib use the fancier ⦃⦄ instead. What is the meaning of ⦃⦄? where is this notation defined (#print notation doesn't seem to help)?

[Reid Barton]

It's not notation, it's builtin syntax (also can be written {{ }}).

[Reid Barton]

I can't find it in TPIL but it means the arguments are not supplied implicitly unless a following explicit argument is given.

[Scott Morrison]

Obviously if there is no following explicit argument at all, {{ }} would be a bad idea. But what are situations where { } ( ) should not be replaced by {{ }} ( )?

[Reid Barton]

Normally it appears on the right hand side of a definition like injective that starts with a forall/Pi type with implicitly quantified variables. Otherwise if you have h : injective f you could not just write h to refer to h.

[Reid Barton]

Hmm, I don't know about that actually.

[Bryan Gin-ge Chen]

Here's the relevant TPiL section.