double curly braces: ∀ ⦃x⦄

Stream: new members

[David Renshaw]

What does ∀ ⦃x⦄ mean? e.g. https://github.com/leanprover-community/mathlib/blob/155b31512b6466fc50c9b6bcce8caecedc218443/src/order/basic.lean#L170

[Kevin Buzzard]

it's an implicit argument but it's not greedily inserted.

[David Renshaw]

ah, I found https://leanprover.github.io/reference/expressions.html#implicit-arguments

[Kevin Buzzard]

See this section of TPIL for more on these weak implicit arguments (including examples of how they might be useful).

[David Renshaw]

thanks!

[Scott Morrison]

I think they are disappearing in Lean 4, so don't fall in love with them!