coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: question (cont.)

From: Vladimir Voevodsky <vladimir AT ias.edu>
To: types-list AT lists.seas.upenn.edu, Coq Club <coq-club AT inria.fr>
Cc: Vladimir Voevodsky <vladimir AT ias.edu>
Subject: [Coq-Club] Re: question (cont.)
Date: Thu, 19 Jul 2012 11:16:38 -0400
Envelope-to: types-list AT lists.seas.upenn.edu, coq-club AT inria.fr, vladimir AT ias.edu

> Don't you have False (as 0=1 for instance) hence not A (as
> A ->False) hence exA (as forall notA -> False), hence everything?

Thanks to everybody who pointed this out to me. I'll have to think whether my
question has a more sensible reformulation.

Vladimir.

[Coq-Club] question (cont.), Vladimir Voevodsky, 07/19/2012
- [Coq-Club] Re: question (cont.), Vladimir Voevodsky, 07/19/2012
  - Re: [Coq-Club] Re: question (cont.), Cody Roux, 07/19/2012
  - Re: [Coq-Club] Re: question (cont.), Arnaud Spiwack, 07/20/2012
    - Re: [Coq-Club] Re: question (cont.), Jean Goubault-Larrecq, 07/20/2012
      - Re: [Coq-Club] Re: question (cont.), Cody Roux, 07/20/2012
        
        Re: [Coq-Club] Re: question (cont.), Jean Goubault-Larrecq, 07/20/2012
      - Re: [Coq-Club] Re: question (cont.), Jean Goubault-Larrecq, 07/20/2012