Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] LEM variants vs. proof relevance

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] LEM variants vs. proof relevance


Chronological Thread 
  • 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.pdfhttps://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




Archive powered by MHonArc 2.6.18.

Top of Page