Documentation on documentation?

Stream: new members

[mars0i]

One of the things I love about Lean is the API documentation system. I'm a beginner though, and I'm still confused about how to read parts of the documentation. (Examples: What are "Equations" and "Instances for"? I have partial guesses about these elements, but I'm not sure.)

Is there a page or paragraph anywhere that spells out the meaning of the different parts of the documentation for a function/theorem/etc.? Maybe it could be linked to from the API documentation and/or Loogle.

[Henrik Böving]

That doesn't exist right now no.

Equations are the equational theorems about the definition that are derived automatically upon defining it.

Instances for are the typeclass instances in which the definition in question occurs

[mars0i]

Thanks @Henrik Böving.

Equations are the equational theorems about the definition that are derived automatically upon defining it.

I don't know enough to recognize what some of the Equations say, so it's helpful to know that they are theorems (that I will hopfully understand better later). Some of the Equations are quite simple.

Instances for are the typeclass instances in which the definition in question occurs

OK. Still learning about some of the details of typeclasses. I think I'll understand this syntax later.