coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Scope of definitions

From: Casteran Pierre <pierre.casteran AT labri.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Scope of definitions
Date: Tue, 04 Jun 2013 09:33:52 +0200
Organization: LaBRI - Université Bordeaux 1 - France

On 04/06/2013 09:28, Terrell, Jeffrey wrote:

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

Hi,
You should use "Let" for local definitions:

Pierre

Definition x : nat := 1.
Print All.
Section P.
Let y : nat := 2.
Definition f z := y * z.
Print All.
End P.
Print All.

Compute (f 9).

[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