coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Lars Dölle <lars.doelle AT on-line.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] Inductive Definition - glitches in the refman, please confirm one of them
Date: Fri, 10 Aug 2018 07:17:24 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=lars.doelle AT on-line.de; spf=None smtp.mailfrom=lars.doelle AT on-line.de; spf=None smtp.helo=postmaster AT ndisco.misc.net
Ironport-phdr: 9a23:okhAEhyjS8zaX5HXCy+O+j09IxM/srCxBDY+r6Qd1OkfIJqq85mqBkHD//Il1AaPAd2Fraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HSbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRHolikJKjA3/mLYhcJ/kK1Wuw6hqQFlzoLIfI2ZKORyc6XAdt0aX2pBWcNRWjRHDIymdYsPFPcKM+het4n5o1sBswa1CA6oBOz10D9InWX60rA90+s/FQHG2BIvEskJsHTStdn1MKYSUearw6XS0DrMcepb1DHg44bGdRAhpOuDXbN2ccfJyEkvERnFjlSKpoD/MTOVzOIAuHWY4ep4Te+jlmoqpgFrrjWuycogkJTFip4Ux1ze9Sh13J45KNm2RUJhf9KoDp9duzuHO4doQs4uWWJltSAnwbMco5G7ZjIFyJE/yh7fdfOHd4+I7wrlVOmMIDd4n25qeLWlixa38Eig0fHzWtOy0FlUsipJitjMtnYT2BzP8sWLV/9w80e71TuO2A3f8PxILVw1mKbBK5Mt3qY8lp8JvkTCGi/2ll/2jKiTdkg8/uin8f7nYq78qpCBMI97lAX+MqAwlcGkBuQ4NBECX2ya+eS6yrLv51D2T6tSgv0sjqbZqIzaJdgcpqOhHwBV1Z8j5w+jADeizdQXhmIKLElFeRKCl4jmIUvCIPH+DfelglSjii1nx/7cPu6pPpKYJX/a1bzlYLxV6khGyQN1w8oMyYhTD+QlKejoEmNvsNjVRks9OhavhergBdF526sZXyeLA6mUdq/f5wzbrtkzKvWBMddG8A32LOIosqa33C0J3GQFdKzs5qM5LXWxH/BoOUKcOCC+hdFEFWYMs0wyQb6y0QHQYXtof3+3GpkEyHQjEov/V9XEQMWpgbqMmiu2TMUPOzJ2T2uUGHKtTL2qHvcBbCXLfZ1nnj0fXr/nTo463leouROok7c=

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