coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT csail.mit.edu>
- To: AUGER Cedric <Cedric.Auger AT lri.fr>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Do I need JMeq?
- Date: Fri, 18 Nov 2011 09:09:28 -0500
AUGER Cedric wrote:
But I guess that this is not as good as Alexandre answer,
since I don't think that JMeq_eq implies UIP.
There is a sense in which [JMeq_eq] and [UIP] are equivalent logically/expressivity-wise. See Section 10.5 of CPDT.
- [Coq-Club] Do I need JMeq?, Gregory Bush
- Re: [Coq-Club] Do I need JMeq?,
Alexandre Pilkiewicz
- Re: [Coq-Club] Do I need JMeq?,
AUGER Cedric
- Re: [Coq-Club] Do I need JMeq?, Adam Chlipala
- Re: [Coq-Club] Do I need JMeq?, Gregory Bush
- Re: [Coq-Club] Do I need JMeq?,
AUGER Cedric
- Re: [Coq-Club] Do I need JMeq?,
Alexandre Pilkiewicz
Archive powered by MhonArc 2.6.16.