The Coq mailing list

[bertot <(e29315a54f%hidden_head%e29315a54f)Yves.Bertot(e29315a54f%hidden_at%e29315a54f)inria.fr(e29315a54f%hidden_end%e29315a54f)>]

On 13/5/12 11:38 PM, Patricia Peratto wrote:

From which address I can download the coq's libraries

to use them in the CoqIde?

Regards

Patricia

Your question feels strange.  Normally, when Coqide is installed on your machine, the main standard libraries of Coq are also installed.

If Coqide is present on your machine, when you run it, there should be a window with three sub-windows, a tall one on the left, and two smaller ones, on top of one another on the right.   The following text should appear on the right:

<<<<
Welcome to CoqIDE, an Integrated Development Environment for Coq

You are running the Coq Proof Assistant version 8.3pl2 (August 2011)

If the version changes a little (you may have a more recent patch level) it is okay.
>>>>

Now, if you click in the tall window on the left, you should be able to type in some text.  I suggest you
type


Require Import Arith.

(beware of the use of large case and small case letters, also there is a dot at the end of the line).

Then, you can click on the icon that represents an arrow pointing downwareds, which appears above
this tall window.  The effect should be some text appears on the right.

<<<<
[Loading ML file z_syntax_plugin.cmxs ... done]
[Loading ML file quote_plugin.cmxs ... done]
[Loading ML file newring_plugin.cmxs ... done]
>>>>

If that works, then indeed the libraries are already present on you computer.  For instance, you can view some of the theorems present in this library with the following command:

SearchPattern (_ + _ <= _ + _).

The answer that appears on the right contains the following lines:

<<<<
plus_le_compat_r: forall n m p : nat, n <= m -> n + p <= m + p
plus_le_compat_l: forall n m p : nat, n <= m -> p + n <= p + m
plus_le_compat: forall n m p q : nat, n <= m -> p <= q -> n + p <= m + q
>>>>

I hope this helps,

Yves