coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Burak Ekici <ekcburak AT hotmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] -type-in-type option
- Date: Thu, 23 May 2019 15:04:14 +0000
- Accept-language: tr-TR, en-US
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ekcburak AT hotmail.com; spf=Pass smtp.mailfrom=ekcburak AT hotmail.com; spf=Pass smtp.helo=postmaster AT EUR02-HE1-obe.outbound.protection.outlook.com
- Ironport-phdr: 9a23:VxYlCxWMrQhA9QmV/IH3NyYqSdbV8LGtZVwlr6E/grcLSJyIuqrYbBCFt8tkgFKBZ4jH8fUM07OQ7/m5HzVZvd3R7DgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrsAndrNQajZZtJ6o+yRbErWZDdvhLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklDsLOjgk+2zMlMd+kLxUrw6gpxxnwo7bfoeVNOZlfqjAed8WXHdNUtpNWyBEBI63cokBAPcbPetAr4fzuUYArQewCwevGOzhxTBHi2Tq3aIhz+gtDR3K0BAiEt8IrX/arM/1NKAXUe2t0aTI0C/DYOlV2Tzg54bIcREhru2NXbltdsfe10ovGB/egVWNs4zqJTCV2/8Ns2ic8+pgUPigi28jqw1rvjevwcIsh5DPi4kIyV7E7T10zYkpKdGiTEN3f8SoHZpTui2AKod6XNsuQ292tys51rELvJu2fCYWxJkoxBPSbuGIfoyL7x3+UeueOy13iXN7dL+6mhm/8UetxvP6W8KpylhFtDBFncPJtn0V1xzc9MyHSvxl80mu1zmByxzf5v9dLU42mqTXNoctwrkrmZUNq0jDGTL2mFntg6+Ra0Uk/PWn5/7/YrX8oZ+cK5F7hR3iMqQvncy/B/40Mg8TX2iH/eS807rj/U7jTLpWif02l7HVsJHcJcsFuq60GwBY3po55xu7ETuqytUVkHodIF5YZh6Ll43pNEvPIPD8A/e/mVOskDJzyv/YPb3uHo7CLmXZkLj7frZw8E5cyA0vzdBa/Z1UC7UBLOjvVU/2sdzUFgU5PBCsw+b7FNV90ZsTVn6IAq+AKa/drVuI5v80LOSXf48UuDP9K+A/6PL0jH85n0Udfaiz0pcNZnC4BKcuH0LMSn31yvwFDG1C6gE5VanhjECIeT9VfXe7GawmsGIVEoWjWK3eXImuyJGC3Sy6VslbZWtMF0qFEl/ocJmBUvYILimVJ5kywXQ/SbG9Rtp5hlmVvwjgxu8id7KMo3FKhdfYzNFwotbru1Qq7zUtVJad1H2IRmBw2GgPQm1uhfEtkQlG0l6GlJNArbldHN1X6elOV15hZ57b0+lzCtS0UQXELI7QFQSWB+6+CDR0deofht8DZ0EhRIePsyqbhW+KLuZQkLaGQpsp7qjbwn79Yd5nzGrL37UgiF9gRdZTMWqhheh08A2BXoM=
Dear all,
What exactly the "type-in-type" option is doing? My vague understanding
is that it disables universe consistency checks and allows for
inconsistent construction of large types. Is that the case? I wonder if
it is making Coq inherently inconsistent or just unsafe?
Thanks a lot!
Best,
―
Burak.
- [Coq-Club] -type-in-type option, Burak Ekici, 05/23/2019
- Re: [Coq-Club] -type-in-type option, Matthieu Sozeau, 05/30/2019
Archive powered by MHonArc 2.6.18.