coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] LEM variants vs. proof relevance
- Date: Sun, 29 May 2016 16:41:43 +0000
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f51.google.com
- Ironport-phdr: 9a23:OuDlARMkwvom4d4BMcol6mtUPXoX/o7sNwtQ0KIMzox0KP/zrarrMEGX3/hxlliBBdydsKIVzbeP+Pm4AyQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTmkb3rsMSLOU1hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv50IbaKvdKMhCLdcET4OMmYv5cStuwOQYxGI4y4+W34RlFJnGQ/e91muXJ7qtS31rO1mw3iyMsj/TLRyUjOnufQ4ACT0gTsKYmZquFrcjdZ92fpW
If you google "private inductive types coq", you get things like https://coq.inria.fr/files/coq5-slides-bertot.pdf, https://coq.inria.fr/files/coq5_submission_3.pdf, and http://www.crm.cat/en/Activities/Documents/barras-crm-2013.pdf, which might be preliminary "documentation"
On Sun, May 29, 2016 at 10:18 AM Jonathan Leivent <jonikelee AT gmail.com> wrote:
On 05/29/2016 10:11 AM, Jason Gross wrote:
> You can throw it in Prop if you want it to be erased in extraction (and
> then the eliminator also has to target Prop). I believe the private
> inductive semantics forbid any new pattern matches outside the module. At
> worst, this will break subject reduction (vm_compute might reject a well
> typed term, unfolding the induction scheme on neutral terms won't work
> nicely), but it won't lead to inconsistency.
Thanks, Jason. I'll consider trying that.
Is Private documented anywhere? I can't find any mention of it in the
refman, and no usage in the standard library.
-- Jonathan
- [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/28/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Gérard Huet, 05/28/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/28/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/28/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Arnaud Spiwack, 05/28/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/28/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jason Gross, 05/29/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/29/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jason Gross, 05/29/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/29/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jason Gross, 05/29/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jason Gross, 05/29/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/28/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/30/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jason Gross, 05/30/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Arnaud Spiwack, 05/28/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/28/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Jonathan Leivent, 05/28/2016
- Re: [Coq-Club] LEM variants vs. proof relevance, Gérard Huet, 05/28/2016
Archive powered by MHonArc 2.6.18.