coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [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
- Re: [Coq-Club] Scope of definitions, Pierre Courtieu, 06/05/2013
Archive powered by MHonArc 2.6.18.