coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Théo Zimmermann <theo.zimmi AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Inductive Definition - glitches in the refman, please confirm one of them
Date: Mon, 20 Aug 2018 16:06:11 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua1-f42.google.com
Ironport-phdr: 9a23:3ZQvWhBYSLkFmekK+XVIUyQJP3N1i/DPJgcQr6AfoPdwSPT7o8bcNUDSrc9gkEXOFd2Cra4c1ayO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUhTexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoIODA5/2PXhMJ+j6xVvQyvqABkzoHOfI2YLuBzcr/Bcd4YQ2dKQ8ZfVzZGAoO5d4YBEeoBOvxfr4blpFQOrB6+BQyyC+P1zz9HnHn23asn2OkmDQHG3BIvH9UUvHXVrdX1MaISUeGuwanHyDXMdfJW2TPn5IfUdRAhpOiBULRtesTfzkkvEhnKjlSWqYH9MDOV1/gNs2yB4OV7T+6gl2knqwRprjiuwMcskIjJiZgPxlDK7yV12Ik1JdykSE57fN6rC4FcuD2dN4tzWs8iTGBouDo6yr0bopG3ZjIGx4ggxx7abfGMbouG4gr7WeqPPTt1gGhpdbG/ihqo70Ss1PPwWtO73VpUqCdOj8PCuWoX1xPJ78iKUvt98Vml2TaIzw3T7/tLIUEwlabCNp4u2KM8moMdsUnMACP6gkr2jKiRdkUr/uin9f7rbanhpp+ZL4N0iwf+PboymsGnH+g0LgwDU3KY9Om8zrHv41P1TKtQgvA5jKXVqJXaKt4apq69DQ9VyIEj6xOnAje60NQXg34HIEhEeRKGiojpPlDOLev3Dfe6mVuskTNry+raMb3mB5XBNmLDn6v5fbZh905czxI+wsxY55JNE70OPPbzWlLqu9HDFR84Mwm0w/79B9ln14MeX3iPAq6DP6/Iv1+I/LFnH+7Zb4gM/T35NvIN5vj0jHZ/l0VOU7Ou2M4raPG/KcZnJkCUe3/lhNFJRXsKsw14Xu3vjVyqXjtaZnL0VKU5sGJoQLm6BJvOE9j+yIeK2z22S8UPNzJ2T2uUGHKtTL2qHvIFaSacOMhky2VWWr2oSotn3har5lajl+hXa9HM8yhdjqrNkcBv7rSKxx43/D1wSc+a1jPVFjwmriYzXzYzmZtHjwl9x1OEi/UqhvVZEZlO7qoMXFtgc5HbyON+Bpb5XQeTJto=

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

Le lun. 20 août 2018 à 14:16, Lars Dölle <lars.doelle AT on-line.de> a écrit :

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

[Coq-Club] Inductive Definition - glitches in the refman, please confirm one of them, Lars Dölle, 08/10/2018
- Re: [Coq-Club] Inductive Definition - glitches in the refman, please confirm one of them, Théo Zimmermann, 08/20/2018