coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Valentin ROBERT <vrobert AT cs.ucsd.edu>
- To: Marcus Ramos <mvmramos AT gmail.com>
- Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Fwd: intros x [H1 | H1]
- Date: Mon, 3 Jun 2013 10:28:52 -0700
Hello Marcus,
This pattern is described here:
(the "a disjunction of lists of patterns" part is relevant)
It basically allows you to destruct the introduced element as it is being introduced. Here the argument following x seems to be of a type with two constructors containing one element each (something like sum or sumbool). The syntax is similar to what you can use with the tactic destruct for instance.
It should therefore leave you in a state with two subgoals, each one containing a hypothesis H1 accounting for the two possibilities.
- Valentin
On Mon, Jun 3, 2013 at 10:22 AM, Marcus Ramos <mvmramos AT gmail.com> wrote:
Hi,
I am new here, trying to lean the basics of Coq, and have already successfully
proved a few very simple theorems. However, I can´t manage to find a solution
for the first part of exercise 5.9 of "Interactive Theorem Proving..." (page
124). The solution shows the use of:
intros x [H1 | H1]
Although I understand "intros x" and the other tactics used in the solution, I
have no idea what the meaning of the [H1 | H1] next to it is. I have tried to
find it in the documentation, however without success. Can anyone explain this
to me?
Thanks in advance,
Marcus.
- [Coq-Club] Fwd: intros x [H1 | H1], Marcus Ramos, 06/03/2013
- Re: [Coq-Club] Fwd: intros x [H1 | H1], Valentin ROBERT, 06/03/2013
- Re: [Coq-Club] Fwd: intros x [H1 | H1], AUGER Cédric, 06/04/2013
- Re: [Coq-Club] Fwd: intros x [H1 | H1], Robbert Krebbers, 06/04/2013
- Re: [Coq-Club] Fwd: intros x [H1 | H1], AUGER Cédric, 06/05/2013
- Re: [Coq-Club] Fwd: intros x [H1 | H1], Robbert Krebbers, 06/05/2013
- Re: [Coq-Club] Fwd: intros x [H1 | H1], Arnaud Spiwack, 06/05/2013
- Re: [Coq-Club] Fwd: intros x [H1 | H1], AUGER Cédric, 06/05/2013
- Re: [Coq-Club] Fwd: intros x [H1 | H1], Robbert Krebbers, 06/04/2013
- Re: [Coq-Club] Fwd: intros x [H1 | H1], AUGER Cédric, 06/04/2013
- Re: [Coq-Club] Fwd: intros x [H1 | H1], Adam Chlipala, 06/03/2013
- Re: [Coq-Club] Fwd: intros x [H1 | H1], Marcus Ramos, 06/05/2013
- Re: [Coq-Club] Fwd: intros x [H1 | H1], Valentin ROBERT, 06/03/2013
Archive powered by MHonArc 2.6.18.