coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How can I make this reasoning step in Coq ?

From: Edsko de Vries <Edsko.de.Vries AT cs.tcd.ie>
To: Matej Kosik <kosik AT fiit.stuba.sk>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] How can I make this reasoning step in Coq ?
Date: Thu, 23 Apr 2009 16:53:29 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

I have chosen unfortunate notation. I thought, it is obvious. E was
meant as a "environment" (set of hypotheses) from which we want to prove
succedent. E is not a proposition.

What is the difference? :)

Edsko

[Coq-Club] How can I make this reasoning step in Coq ?, Matej Kosik
- Re: [Coq-Club] How can I make this reasoning step in Coq ?, Edsko de Vries
  - Re: [Coq-Club] How can I make this reasoning step in Coq ?, Yves Bertot
  - Re: [Coq-Club] How can I make this reasoning step in Coq ?, Matej Kosik
    - Re: [Coq-Club] How can I make this reasoning step in Coq ?, Edsko de Vries
      - Re: [Coq-Club] How can I make this reasoning step in Coq ?, Matej Kosik
        
        Re: [Coq-Club] How can I make this reasoning step in Coq ?, Tillmann Rendel
- Re: [Coq-Club] How can I make this reasoning step in Coq ?, Ezra Cooper