search

leanprover / theorem_proving_in_lean4

Theorem Proving in Lean 4
https://leanprover.github.io/theorem_proving_in_lean4/
Apache License 2.0
153 stars 82 forks source link

Anonymous constructor notation #29

Open ydewit opened 2 years ago

ydewit commented 2 years ago

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 commented 2 years ago

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