Possible mistake in Theorem Proving online docs?

Stream: lean4

[Tom]

Hi, I'm reading the second chapter of "Theorem Proving in Lean 4". In the section

https://leanprover.github.io/theorem_proving_in_lean4/propositions_and_proofs.html#propositions-as-types

The example doesn't seem to work; specifically, Implies is not defined. I can navigate to the other types (And, Or etc) but I can't find Implies (or another similar spelling).

Am I missing something or is this a doc/code problem? Is there a better place to report/discuss documentation issues (GH?)

Thanks!

[Kyle Miller]

I'm not sure what the intention is, but if you click the eye icon it reveals the definition def Implies (p q : Prop) : Prop := p → q

[Kevin Buzzard]

"Copy to clipboard" also seems to copy the def, even though it's invisible.

[Mario Carneiro]

Note the text:

For example, we could introduce a new type, Prop, to represent propositions, and introduce constructors to build new propositions from others.

This is talking about a way lean could be set up, which is not the actual setup

[Mario Carneiro]

the eye shows additional hidden setup needed to make the displayed text typecheck