Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Scope of definitions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Scope of definitions


Chronological Thread 
  • From: Adam Chlipala <adamc AT csail.mit.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Scope of definitions
  • Date: Tue, 04 Jun 2013 05:13:23 -0400

On 06/04/2013 03:28 AM, Terrell, Jeffrey wrote:
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?

Making definitions with global scope (or at least outside-the-section scope) is precisely the purpose of Coq sections. Perhaps it's worth having look at the manual or another introduction to sections.



Archive powered by MHonArc 2.6.18.

Top of Page