Anonymous constructor notation

[ydewit]

It seems that there are two different notations for anonymous constructors:

instance : ToString Rules := { toString := fun rs => "TBD" }

and

instance : ToString Rules := ⟨ fun rs => "TBD" ⟩

The former is defined in the the Structures and Records > Objects and the latter somewhere in Quantifiers and Equality > The Existencial Quantifier.

(1) Shouldn't both anonymous constructors be documented together as two different ways to construct structures or inductive types?

(2) Should there be, at least, a link to this anonymous constructor documentation in the inductive types section too?

[lovettchris]

I was going to file this bug also, would love to see the anonymous constructor notation also mentioned in structures and records.