Implicit arguments in Equivalence

Stream: lean4

[Dan Velleman]

I have two questions about the implicit arguments in the definition of Equivalence in Lean.Init.Core.

1. symm and trans use {...}. Should they be {{...}}? That's what was used in the definitions of symmetric and transitive in Lean 3.
2. Suppose I have e : Equivalence r. Then the type of e.symm is ∀ {x y}, r x y → r y x. Suppose I want to specify the arguments explicitly. It seems like I should be able to use @e.symm, or perhaps @(e.symm), but that doesn't seem to work. What's the correct syntax to get something that acts like ∀ (x y), r x y → r y x?

[Jireh Loreaux]

1. It's possible Equivalence was around before semi-implicit arguments existed in Lean 4, I'm not sure though. (Hmmm.... Interesting to note that Symmetric uses semi-implicits)
2. fun _x _y => e.symm works.