coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How to understand "Declare" in a module?

From: Hai WAN <wan.whyhigh AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] How to understand "Declare" in a module?
Date: Tue, 2 Feb 2010 19:55:59 +0800
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=DsdAS7fbSS5xsjWHk0gmUHM7B8pT7yCclEtTeuEaBZAAoMh9NNLihFHhl43bu+3Iop fQVZmAQQ0rEAzE2ql4upsgw7UB5pw9hU5d3kEOjBMTfHEqN5lPoNTXVoCTYyL+c+zTGq LhEJ5aXsy8h0XQuIyyFKp6nBRkUQhf51jEInQ=

Dear all,

Suppose we have the following codes:

---------------------------------------------------

Module Type F_sig.

Axiom F : False.

End F_sig.

Module F_mod.

Declare Module f : F_sig.

Theorem ff :
� False.
apply f.F.
Qed.

End F_mod.

---------------------------------------------------

What does it mean by "Declare Module f : F_sig.". Does it mean that we declare a module f of signiture F_sig? Is it similar to "Variable f : F_sig"?

I then wrote the following codes, which make totally confused.

---------------------------------------------------

Goal False.
apply F_mod.ff.
Qed.

---------------------------------------------------

Can anyone help?

--
Best regards,
Hai WAN

[Coq-Club] How to understand "Declare" in a module?, Hai WAN
- Re: [Coq-Club] How to understand "Declare" in a module?, Adam Chlipala