[Coq-Club] Inductive Definition - glitches in the refman, please confirm one of them

[Lars Dölle]

Hi,

reading the section titled "Inductive Defintions" in reference manual,

| https://coq.inria.fr/distrib/current/refman/language/cic.html#inductive-definitions

a parameter "p" is introduced. Then three examples follow, namely
"list", "tree+forest", "even+odd".

I see some glitches here:

0) In the Web-page, end of last paragraph before the formal representation
of "list", a text "** Examples **" appears, which should be sub-section title,
i think.

1) In the formal representation of "tree+forest", the parameter p is
missing. The text spells "Ind[]", but it should be "Ind[0]".

2) I think, in the "even+odd" formal representation, the parameter p
also wrong. The text spells "Ind[1]", but it should be "Ind[0]" to the
best of my understanding. The point is that

| even_O : even 0

does not have a parameter. It would help me, if someone could please
confirm my reading here.

3) In the example of "even+odd", "Prop" is spelled in small letters "prop",
thus one cannot copy-paste the text into coqide.

Thanks and kind regards

Lars

[Théo Zimmermann]

Hi Lars,

Thank you for your report. Note that you have much better chances to get a
follow up of this kind of remarks by opening a new issue on the Coq bug
tracker (https://github.com/coq/coq/issues).

You are correct in all the glitches you noticed, and in fact, the first
three (0, 1 and 2) were already fixed by previous contributors.
Unfortunately though, the version of the manual that is present on the
website is only updated at release time (8.8.2 should happen rather soon I
think), although there are plans to put in place some continuous deployment
of the documentation. For the moment, you can generally find the
documentation for the development branch at
https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=documentation
(disclaimer: can be slower to load).

The last glitch you noticed (casing of Prop) hadn't been noticed / fixed
yet. Would you like to open a pull request fixing it? The code to change
can be found at
https://github.com/coq/coq/blob/master/doc/sphinx/language/cic.rst.

Kind regards,
Théo

Post by Lars Dölle
Hi,
reading the section titled "Inductive Defintions" in reference manual,
|
https://coq.inria.fr/distrib/current/refman/language/cic.html#inductive-definitions
a parameter "p" is introduced. Then three examples follow, namely
"list", "tree+forest", "even+odd".
0) In the Web-page, end of last paragraph before the formal representation
of "list", a text "** Examples **" appears, which should be sub-section title,
i think.
1) In the formal representation of "tree+forest", the parameter p is
missing. The text spells "Ind[]", but it should be "Ind[0]".
2) I think, in the "even+odd" formal representation, the parameter p
also wrong. The text spells "Ind[1]", but it should be "Ind[0]" to the
best of my understanding. The point is that
| even_O : even 0
does not have a parameter. It would help me, if someone could please
confirm my reading here.
3) In the example of "even+odd", "Prop" is spelled in small letters "prop",
thus one cannot copy-paste the text into coqide.
Thanks and kind regards
Lars