coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Question about inductive definitions

From: "N. Raghavendra" <nyraghu27132 AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Question about inductive definitions
Date: Fri, 16 Feb 2018 19:31:04 +0530
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=nyraghu27132 AT gmail.com; spf=Pass smtp.mailfrom=nyraghu27132 AT gmail.com; spf=None smtp.helo=postmaster AT mail-pg0-f47.google.com
Ironport-phdr: 9a23:0KgSrRNcPWQMHL9Gaccl6mtUPXoX/o7sNwtQ0KIMzox0Ivr4rarrMEGX3/hxlliBBdydt6ofzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlGiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSkHKTA37WPYisJ+g6JBrhyvpBNwzJLbboyOKPp+Z7nQcc8GSWdbXMtcUTFKDIOmb4sICuoMJehUoZHnq1ATsRWxHwasBOP1xT9WmHD227A10/47Hg3IwQctGNQOsXTOrNrvO6cSUf21wLfKwDneYf5axyzw6IfNch87oPGMWah8ftbWyUkqDg7IiEibp4LiPzOQzOsNsm6b4vJgVeK1im4rsRtxrSa0xss2i4nJgJoZykra+iVl2oY1IsG4R1B0YN64C5tcrSeaOJVqQs4kXmpmuz46x6UEtJO0ZiQG1Yoryh7FZ/GEfYWE+B3uWeSJLTtli39pYq+zihi2/ES6yuDxUtO43EtFoyZZlNTHq2oD2AbJ6sedT/tw5keh1iiL1wDU8uxEJFo7lavfK5I42r4wmYYfvV3NHiL5mkj6lqCWdkIj+uin7+TofK/qqYObN49xkg3+M6IuldKjAekgMAUDUHKX9fmi2LDj50H0Q7tHguc5n6TbqJzaIN4Upq+9Aw9byIYj7BO/Ai+g0NUYh3kINl1FeBKaj4T3OVzCPf71AemkjlSjlTdk3fHGPrn7DprRKXjDla/tfaxh5E5E1Aoz0ddf6opIBbEGOfL/Q1P+tNjFDhAiKAG02ObmCNBl1owEQ26PA6mZMLnTsVCS/O4vLfOMN8cpv2P2LOFg7Przh1c4n0UcdO+nx8gtZWi8D8hhdg+/JzLWi9gBGHkHuAYkRaai3FuTSzdcZ2voAPtnvBk0DYunCcHIQYX705Kb2yLuVLsQLlpPBVCFD3rue5+NEb9YbjOIK8Bhj2ZbDOP7Y4Ak3BCq8gT9zuw0faLv5iQEuMe7h5BO7OrJmERqrG0mP4Gmy2iIClpMsCYNTj4y0rp4pBUkmFiG2Kl8xfdfEI4Kvq8bYkIBLZfZitdCJZXqQAuYJ4WGTV+nRpOtBjRjFotske9LWF50HpCZtj6G3yeuBOVIxbmCBZhx6q2EmnateIByzHHJ0KRnhF4jEJNC

At 2018-02-16T10:57:27+01:00, Gaëtan Gilbert wrote:

> The destructors are different but equivalent, it should be possible to
> define each from the other.

Given that, since the destructor provided by the first definition is
shorter than the one provided by the second one, I guess I'll use the
first definition.

Thanks,
Raghu.

--
N. Raghavendra
<raghu AT hri.res.in>,
http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/

[Coq-Club] Question about inductive definitions, N. Raghavendra, 02/16/2018
- Re: [Coq-Club] Question about inductive definitions, Gaëtan Gilbert, 02/16/2018
  - Re: [Coq-Club] Question about inductive definitions, N. Raghavendra, 02/16/2018