coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Newbie question about 'exists'.

From: Stéphane Glondu <steph AT glondu.net>
To: Bernard Hurley <bernard AT marcade.biz>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Newbie question about 'exists'.
Date: Fri, 30 Mar 2012 07:43:39 +0200
Openpgp: id=49881AD3

Le 29/03/2012 22:58, Bernard Hurley a écrit :
> The proof works OK. However I would have expected to be able to use:
>
> exists (m := n).

Note that you can also do just "exists n".

Cheers,

--
Stéphane

[Coq-Club] Newbie question about 'exists'., Bernard Hurley
- Re: [Coq-Club] Newbie question about 'exists'., Adam Chlipala
- Re: [Coq-Club] Newbie question about 'exists'., Stéphane Glondu