coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] how to prove false

From: Jonathan Leivent <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] how to prove false
Date: Wed, 25 Mar 2015 12:50:21 -0400

On 03/25/2015 12:32 PM, Jacques-Henri Jourdan wrote:

Well, using <: is the same thing as using vm_compute.

I missed this in the refman : "term <: type” locally sets up the virtual machine (as if option Virtual Machine were on, see 6.10.6) for checking that term has type type."

OK - I'm panicking a bit less...

-- Jonathan

[Coq-Club] how to prove false, Stefan Ciobaca, 03/25/2015
- Re: [Coq-Club] how to prove false, Jonathan Leivent, 03/25/2015
  - Re: [Coq-Club] how to prove false, Jacques-Henri Jourdan, 03/25/2015
    - Re: [Coq-Club] how to prove false, Jonathan Leivent, 03/25/2015
      - Re: [Coq-Club] how to prove false, Laurent Théry, 03/25/2015
        
        Re: [Coq-Club] how to prove false, Jonathan Leivent, 03/25/2015
        
        Re: [Coq-Club] how to prove false, Laurent Théry, 03/25/2015
        
        Re: [Coq-Club] how to prove false, Matthieu Sozeau, 03/25/2015