coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Scope of definitions

From: "Terrell, Jeffrey" <jeffrey.terrell AT kcl.ac.uk>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Scope of definitions
Date: Tue, 4 Jun 2013 07:28:44 +0000
Accept-language: en-GB, en-US

Hi,

I was surprised to find that y is still in scope after the section is closed.

Definition x : nat := 1.
Print All.
Section P.
Definition y : nat := 2.
Print All.
End P.
Print All.

Do definitions (as opposed to declarations) always have global scope? If so,
why?

Regards,
Jeff.

[Coq-Club] Scope of definitions, Terrell, Jeffrey, 06/04/2013
- Re: [Coq-Club] Scope of definitions, Casteran Pierre, 06/04/2013
- Re: [Coq-Club] Scope of definitions, Adam Chlipala, 06/04/2013
  - Re: [Coq-Club] Scope of definitions, Pierre Courtieu, 06/05/2013
    - Re: [Coq-Club] Scope of definitions, Terrell, Jeffrey, 06/05/2013