coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gábor Bakos <aborgabor AT gmail.com>
- To: Coq-Club <coq-club AT pauillac.inria.fr>
- Subject: [Coq-Club] FAQ; 8.2
- Date: Sun, 15 Feb 2009 20:40:40 +0000
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=KHyPu5RcvvljKTpboaEIKOIz158QBQsPFWsW+ZHHFhm4Vy0HyJ7x0vNIo2vS1+uRpF ywym7TvGAvAxWhYY9aaalSj1b4EmQeiBfvKajkT+gf/Q+aCymM2ZeTI27BTk5NWfkv58 lQdFcM9njOfqbKuwnB/5k+iIeZA+XWSTR+tAM=
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi All,
(Newbie post, non-native English speaker sorry about it.)
(Sorry if double post, the previous went to the mailto address from the contact page (coq-club_NS AT pauillac.inria.fr) which seems to be not correct. At least it resulted a mail delivery failure.)
I was able to download 8.2 sources from the homepage of Coq yesterday. Was it accidental? The build sais it is 8.2 (February 2009). If I remember well those sources were marked as stable. Was that release revoked or it was just a dream ;)? (I see no signs of 8.2 at the home page of Coq.)
Regarding the FAQ: The question 68 has a little confusing answer. Would not it be better choice what does the error message means? Or finishing by
cut (b*a <>0 -> a<>0).
cut (b*a <>0 -> b<>0).
auto.
auto with real.
auto with real.
Qed.
or
firstorder.
Qed.
?
Some of the questions (ex.: 133, 135, 144) remain unanswered. Are those intentional? (As I remember yesterday these were also unanswered, so it seems to be not a later corrected behaviour.) I am not sure are these should go to the bug tracking system?
I miss an entry regarding the cardinality related formulation. I would like to reason about finite sets' cardinality. Is it well supported? (Actually I am afraid some of the first FAQ answers should answered my question, but I am not as well trained in this field to get the proper conclusion easily.)
The tool seems to be great! Thanks, gabor
PS.: Is not somewhere an eclipse plugin like Proof General for Coq? (It would be interesting to see some of the XText features, like context sensitive completion, content based hilighting, maybe model transformation to MathML, ...)
- [Coq-Club] FAQ; 8.2, Gábor Bakos
Archive powered by MhonArc 2.6.16.