diff options
Diffstat (limited to 'doc/refman/RefMan-ext.tex')
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 41 |
1 files changed, 37 insertions, 4 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 2da5bec1..2c4985c1 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -5,6 +5,8 @@ the Gallina's syntax. \section{Record types \comindex{Record} +\comindex{Inductive} +\comindex{CoInductive} \label{Record}} The \verb+Record+ construction is a macro allowing the definition of @@ -20,10 +22,13 @@ construction allows to define ``signatures''. {\sentence} & ++= & {\record}\\ & & \\ {\record} & ::= & - {\tt Record} {\ident} \zeroone{\binders} \zeroone{{\tt :} {\sort}} \verb.:=. \\ + {\recordkw} {\ident} \zeroone{\binders} \zeroone{{\tt :} {\sort}} \verb.:=. \\ && ~~~~\zeroone{\ident} \verb!{! \zeroone{\nelist{\field}{;}} \verb!}! \verb:.:\\ & & \\ +{\recordkw} & ::= & + {\tt Record} $|$ {\tt Inductive} $|$ {\tt CoInductive}\\ + & & \\ {\field} & ::= & {\name} \zeroone{\binders} : {\type} [ {\tt where} {\it notation} ] \\ & $|$ & {\name} \zeroone{\binders} {\typecstr} := {\term} \end{tabular} @@ -149,6 +154,13 @@ Eval compute in half.(Rat_bottom_cond). Reset Initial. \end{coq_eval} +Records defined with the {\tt Record} keyword are not allowed to be +recursive (references to the record's name in the type of its field +raises an error). To define recursive records, one can use the {\tt + Inductive} and {\tt CoInductive} keywords, resulting in an inductive +or co-inductive record. A \emph{caveat}, however, is that records +cannot appear in mutually inductive (or co-inductive) definitions. + \begin{Warnings} \item {\tt Warning: {\ident$_i$} cannot be defined.} @@ -167,10 +179,16 @@ Reset Initial. \begin{ErrMsgs} -\item \errindex{A record cannot be recursive} +\item \errindex{Records declared with the keyword Record or Structure cannot be recursive.} - The record name {\ident} appears in the type of its fields. - + The record name {\ident} appears in the type of its fields, but uses + the keyword {\tt Record}. Use the keyword {\tt Inductive} or {\tt + CoInductive} instead. +\item \errindex{Cannot handle mutually (co)inductive records.} + + Records cannot be defined as part of mutually inductive (or + co-inductive) definitions, whether with records only or mixed with + standard definitions. \item During the definition of the one-constructor inductive definition, all the errors of inductive definitions, as described in Section~\ref{gal_Inductive_Definitions}, may also occur. @@ -1557,8 +1575,23 @@ but succeeds in Check Prop = nat. \end{coq_example*} +\subsection{Deactivation of implicit arguments for parsing} +\comindex{Set Parsing Explicit} +\comindex{Unset Parsing Explicit} +Use of implicit arguments can be deactivated by issuing the command: +\begin{quote} +{\tt Set Parsing Explicit.} +\end{quote} +In this case, all arguments of constants, inductive types, +constructors, etc, including the arguments declared as implicit, have +to be given as if none arguments were implicit. By symmetry, this also +affects printing. To restore parsing and normal printing of implicit +arguments, use: +\begin{quote} +{\tt Set Parsing Explicit.} +\end{quote} \subsection{Canonical structures \comindex{Canonical Structure}} |