The Coq mailing list

[AUGER <Cedric.Auger AT lri.fr>]

Le Tue, 02 Mar 2010 18:05:17 +0100, Matthieu Sozeau <mattam AT mattam.org> a  
écrit:

> Le 2 mars 10 à 09:59, Vladimir Voevodsky a écrit :
>
> > Suppose I have some local definitions in a section which are introduced  
> > with [Let].  Then they start showing up in the local environments of  
> > all the proofs in the section. How can I ask Coq not to display some of  
> > these definitions on the "goals" pages of the proofs?
>
> Dear Vladimir,
>
>    you can use either [Definition]s or [Notation]s instead of [Let]
> to define abbreviations that won't appear in the proof context.
>
> Hope this helps,
> -- Matthieu

"Notation" is probably best than "Definition", as it will die after the  
"End [Section].";
but if your local definition is big and used many times in each definition,
proof terms will be unnecessary huge.


--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay