From c973bb9c2401880c7aba4ab0b1e3b99c4c8ab39d Mon Sep 17 00:00:00 2001 From: ppedrot Date: Mon, 11 Mar 2013 20:14:38 +0000 Subject: Documentation of the "Local Definition" command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16264 85f007b7-540e-0410-9357-904b9bb8a0f7 --- doc/refman/RefMan-ext.tex | 3 ++- doc/refman/RefMan-gal.tex | 19 ++++++++++++------- doc/refman/RefMan-mod.tex | 16 ++++++++++++++++ 3 files changed, 30 insertions(+), 8 deletions(-) (limited to 'doc/refman') diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 9c7e7d1df..fc511a45c 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -994,7 +994,8 @@ declaration is added to the context. An absolute name is called {\it visible} from a given short or partially qualified name when this latter name is enough to denote it. This means that the short or partially qualified name is mapped to the absolute name in {\Coq} name -table. +table. Definitions flagged as {\tt Local} are only accessible with their +fully qualified name (see \ref{Definition}). A similar table exists for library file names. It is updated by the vernacular commands {\tt Add LoadPath} and {\tt Add Rec LoadPath} (or diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index 588016b0a..64afc1aed 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -446,7 +446,7 @@ expression ``{\tt fun}~{\ident$_{1}$}~{\ldots}~{\ident$_{n}$}~{\tt :}~\type~{\tt =>}~{\term}'' denotes the same function as ``{\tt fun}~{\ident$_{1}$}~{\tt :}~\type~{\tt =>}~{\ldots}~{\tt fun}~{\ident$_{n}$}~{\tt :}~\type~{\tt =>}~{\term}''. If a let-binder -occurs in the list of binders, it is expanded to a local definition +occurs in the list of binders, it is expanded to a let-in definition (see Section~\ref{let-in}). \subsection{Products @@ -508,16 +508,16 @@ Expressions often contain redundant pieces of information. Subterms that can be automatically inferred by {\Coq} can be replaced by the symbol ``\_'' and {\Coq} will guess the missing piece of information. -\subsection{Local definitions (let-in) +\subsection{Let-in definitions \label{let-in} -\index{Local definitions} +\index{Let-in definitions} \index{let-in}} {\tt let}~{\ident}~{\tt :=}~{\term$_1$}~{\tt in}~{\term$_2$} denotes the local binding of \term$_1$ to the variable $\ident$ in \term$_2$. -There is a syntactic sugar for local definition of functions: {\tt +There is a syntactic sugar for let-in definition of functions: {\tt let} {\ident} {\binder$_1$} {\ldots} {\binder$_n$} {\tt :=} {\term$_1$} {\tt in} {\term$_2$} stands for {\tt let} {\ident} {\tt := fun} {\binder$_1$} {\ldots} {\binder$_n$} {\tt =>} {\term$_2$} {\tt in} @@ -698,7 +698,7 @@ definition have a special syntax: ``{\tt let fix}~$f$~{\ldots}~{\tt &&\\ %% Definitions {\definition} & ::= & - {\tt Definition} {\ident} \zeroone{\binders} {\typecstr} {\tt :=} {\term} {\tt .} \\ + \zeroone{\tt Local} {\tt Definition} {\ident} \zeroone{\binders} {\typecstr} {\tt :=} {\term} {\tt .} \\ & $|$ & {\tt Let} {\ident} \zeroone{\binders} {\typecstr} {\tt :=} {\term} {\tt .} \\ &&\\ %% Inductives @@ -878,6 +878,11 @@ environment, provided that {\term} is well-typed. {\tt fun}\,{\binder$_1$} {\ldots} {\binder$_n$}\,{\tt =>}\,{\term$_2$}\,% {\tt .} +\item {\tt Local Definition} {\ident} := {\term}\\ +\comindex{Local Definition} + Such definitions are never made accessible through their unqualified name by + {\tt Import} and its variants (see \ref{Import}). You have to explicitly + give their fully qualified name to refer to them. \item {\tt Example {\ident} := {\term}.}\\ {\tt Example} {\ident} {\tt :} {\term$_1$} {\tt :=} {\term$_2$}{\tt .}\\ {\tt Example} {\ident} {\binder$_1$} {\ldots} {\binder$_n$} @@ -899,7 +904,7 @@ This command binds the value {\term} to the name {\ident} in the environment of the current section. The name {\ident} disappears when the current section is eventually closed, and, all persistent objects (such as theorems) defined within the -section and depending on {\ident} are prefixed by the local definition +section and depending on {\ident} are prefixed by the let-in definition {\tt let {\ident} := {\term} in}. \begin{ErrMsgs} @@ -1616,7 +1621,7 @@ and {\tt Transparent}) and~\ref{unfold} (tactic {\tt unfold}). \item {\tt Let {\ident} \zeroone{\binders} : {\type}.} Like {\tt Definition {\ident} \zeroone{\binders} : {\type}.} except -that the definition is turned into a local definition generalized over +that the definition is turned into a let-in definition generalized over the declarations depending on it after closing the current section. \item {\tt Fixpoint \nelist{{\ident} {\binders} \zeroone{\annotation} {\typecstr} \zeroone{{\tt :=} {\term}}}{with}.} diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex index 68d572265..f4a90740c 100644 --- a/doc/refman/RefMan-mod.tex +++ b/doc/refman/RefMan-mod.tex @@ -372,6 +372,22 @@ Some features defined in modules are activated only when a module is imported. This is for instance the case of notations (see Section~\ref{Notation}). +Declarations made with the {\tt Local} flag are never imported by the +{\tt Import} command. Such declarations are only accessible through their +fully qualified name. + +Example: + +\begin{coq_example} +Module A. +Module B. +Local Definition T := nat. +End B. +End A. +Import A. +Check B.T. +\end{coq_example} + \begin{Variants} \item{\tt Export {\qualid}}\comindex{Export} -- cgit v1.2.3