Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Impredicative Set

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Impredicative Set


Chronological Thread 
  • From: Théo Zimmermann <theo.zimmi AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Impredicative Set
  • Date: Fri, 15 Mar 2019 21:29:21 +0100
  • Authentication-results: mail2-smtp-roc.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-vs1-f48.google.com
  • Ironport-phdr: 9a23:pr4/DhWCKlCbi0A4zoPMX8QRutfV8LGtZVwlr6E/grcLSJyIuqrYYx2Ft8tkgFKBZ4jH8fUM07OQ7/m4HzRZqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5uIBmssQndq9QdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KpwVhTmlDkIOCI48GHPi8x/kqRboA66pxdix4LYeZyZOOZicq/Ye94RWGhPUdtLVyFZDYy8YYkAAeoPM+hbsofzuUcBoACkCgWwHu7i0CNEimP00KA8zu8vERvG3AslH98WrnrUrM/yNKAKXu+2zanIyDDDYO1M2Tf48ofIdBYhquyLULJsccre104vGxnEj1WRrIzlOjKV2/8Cs2ie9eVgVOavh3Q7pAF2pzii38EhgZTHiIISz1DL7yR5wIAtKN23SU57fd6kEIZLuC2AK4R2RcYiTmd1syg50r0LoYC3cDQOxZg9xBPSa+aLf5aV7h/hTuqcLjR1iXR4c7ylnRmy61KvyujkW8m0zllKqi1Fn8HJtn8X1hzT7tGLSuVm/ku8wDqP2Q/e5+JeLUA7kqrbLJEhwroumZYJrUvDGSr2lF33jK+QaEok5vCl5/r7brjivJORNI95hhvgPqgzmMGzG+s1PwsWU2ie4+u81bnj/UPjQLVNi/07irXZsJDEKsQcvKK4Ag5V0oMm6xa+FDqm39EYkmMGLFJBYh6Ik4/pO1TWLPDiEfi/m0iskCtsx/3eIrLhBYzNImHfn7flYLZy8FVRyBEzzNBa/5JbEKsNIPP1Wk/rtdzXFAU1MwKuw7WvNNIo/YQHEUmLH6XRZKjVqBqD4v8lC+iKfo4c/jjnfasL/fnr2EM5GFgqT6is2JYNbXm+GLwyP0WUZjz+g9IEEE8FuwM/SKrhj1jUAm0bXGq7Q69pvmJzM4mhF4qWA9n12OXQjhf+JYVfYyV9Mn7JFH7pc4ueXPJVMXCdJ8ZglnoPUr3zEtZ9hyHrjxfzzv9cFsSR4jcR7Mux29185umVnhY3p2QtUpatllqVRmQxpVsmAj872Kcl/B54w1aHlLZj2rlWSYwV6PROXQM3c5Xbyr4iBg==

Related: https://github.com/coq/coq/issues/9458

Le ven. 15 mars 2019 à 20:26, Stefan Monnier <monnier AT iro.umontreal.ca> a écrit :
> I am wondering how “sketchy” the use of impredicative Set in Coq
> developments is considered.

I'm not in a position to weigh in on this aspect, but my experience with
it has been rather disappointing: the restrictions imposed on it to
avoid inconsistencies (namely the inability to perform strong
eliminations on such large Set types) renders them frustrating, because
you can define interesting datatypes and functions on them, but very
often you can't then prove properties of those functions (at least not
without adding ad-hoc axioms whose soundness is at best unknown).


        Stefan



Archive powered by MHonArc 2.6.18.

Top of Page