Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] question about universes and equalities

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] question about universes and equalities


Chronological Thread 
  • From: Stefan Monnier <monnier AT iro.umontreal.ca>
  • To: Jason Gross <jasongross9 AT gmail.com>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] question about universes and equalities
  • Date: Mon, 09 May 2016 15:48:22 -0400
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=monnier AT iro.umontreal.ca; spf=SoftFail smtp.mailfrom=monnier AT iro.umontreal.ca; spf=None smtp.helo=postmaster AT ironport2-out.teksavvy.com
  • Ironport-phdr: 9a23:D+owRhLPqenJmWNZx9mcpTZWNBhigK39O0sv0rFitYgUIvjxwZ3uMQTl6Ol3ixeRBMOAu6MC0rCd6vu/EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35Xxjrr5osaMKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46Fp34d6XK77Z6U1S6BDRHRjajhtpZ6jiR6WbwKU4X1UfX8RiQEAVwrM9xb8UY32qTCrnuV40Siee8bxSOZndy6l6vJQVBLmgSFPEjk/9mDakIQkiaVdphOsvTR+2YmSfYSSMuZkc6rZO9gTEzkSFv1NXjBMV9vvJ7AECPAMaKMB99Hw
> Note that [@eq Type@{i} A B -> @eq Type@{j} A B] does not hold for [i > j],

Hmm.. which part of Coq's typing rules cause this?


Stefan

Archive powered by MHonArc 2.6.18.

Top of Page