coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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==
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
- [Coq-Club] Impredicative Set, Jay Kruer, 03/15/2019
- Re: [Coq-Club] Impredicative Set, Stefan Monnier, 03/15/2019
- Re: [Coq-Club] Impredicative Set, Théo Zimmermann, 03/15/2019
- Re: [Coq-Club] Impredicative Set, Jean-Francois Monin, 03/15/2019
- Re: [Coq-Club] Impredicative Set, Théo Zimmermann, 03/15/2019
- Re: [Coq-Club] Impredicative Set, Stefan Monnier, 03/15/2019
Archive powered by MHonArc 2.6.18.