coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] "intuition except" ?

From: Pierre Courtieu <Pierre.Courtieu AT univ-orleans.fr>
To: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] "intuition except" ?
Date: Mon, 11 Apr 2005 10:25:14 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On 08 avr 2005, jandronick wrote:

> intros. split.
>     decompose [and] H; apply R_def; auto.
>     intuition.
>       left; apply P_succ; auto.
>       right; apply Q_succ_succ; auto.
> --------
> But if I have the hypotheses, and the goal, with a lot of "and" and "or"
> and  "exists" etc... it becomes heavy !!!

Not so heavy because you can do : "decompose [and or ex] H; ..."

Pierre.

[Coq-Club] "intuition except" ?, jandronick
- Re: [Coq-Club] "intuition except" ?, Pierre Casteran
  - Re: [Coq-Club] "intuition except" ?, jandronick
    - Re: [Coq-Club] "intuition except" ?, Pierre Courtieu