coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Aleksandar Nanevski <aleks.nanevski AT imdea.org>
- To: Vladimir Voevodsky <vladimir AT ias.edu>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] reasoning out of type equalities
- Date: Sun, 05 Aug 2012 14:45:41 +0200
- Organization: IMDEA Software Institute
Interesting. Ok, what if nonempty B is defined as (exists v : B, True), rather than as (B <> False)? -Aleks On 8/5/12 2:20 PM, Vladimir Voevodsky
wrote:
No.
not((A or (not A)) = False) <-> not(not(A or (not A))
<-> not ((not A) and A) <-> not(False) <->
True.
V.
On Aug 5, 2012, at 7:48 AM, Aleksandar Nanevski wrote:
|
- [Coq-Club] reasoning out of type equalities, Aleks Nanevski, 08/04/2012
- Message not available
- Re: [Coq-Club] reasoning out of type equalities, Kristopher Micinski, 08/04/2012
- Message not available
- Re: [Coq-Club] reasoning out of type equalities, Chung-Kil Hur, 08/04/2012
- Re: [Coq-Club] reasoning out of type equalities, Vladimir Voevodsky, 08/04/2012
- Re: [Coq-Club] reasoning out of type equalities, Aleksandar Nanevski, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, andré hirschowitz, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Aleksandar Nanevski, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Vladimir Voevodsky, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Aleksandar Nanevski, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Vladimir Voevodsky, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Aleksandar Nanevski, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Adam Chlipala, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Aleksandar Nanevski, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, andré hirschowitz, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Vladimir Voevodsky, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Vladimir Voevodsky, 08/06/2012
- Re: [Coq-Club] reasoning out of type equalities, Aleksandar Nanevski, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Vladimir Voevodsky, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Aleksandar Nanevski, 08/05/2012
Archive powered by MHonArc 2.6.18.