aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rwxr-xr-xdoc/common/macros.tex1
-rw-r--r--doc/refman/RefMan-ext.tex26
2 files changed, 23 insertions, 4 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index f0fb0883b..ce998a9bc 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -206,6 +206,7 @@
%END LATEX
%HEVEA \renewcommand{\proof}{\nterm{proof}}
\newcommand{\record}{\nterm{record}}
+\newcommand{\recordkw}{\nterm{record\_keyword}}
\newcommand{\rewrule}{\nterm{rewriting\_rule}}
\newcommand{\sentence}{\nterm{sentence}}
\newcommand{\simplepattern}{\nterm{simple\_pattern}}
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 0cfdbe17b..2c4985c15 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.