diff options
| -rw-r--r-- | doc/RefMan-gal.tex | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex index e856566c7..0696f1702 100644 --- a/doc/RefMan-gal.tex +++ b/doc/RefMan-gal.tex @@ -963,7 +963,7 @@ Reset Initial. \begin{Variants} \item \begin{coq_example*} -Inductive list (A:Set) : Set := nil | cons (_:X) (_:list X). +Inductive list (A:Set) : Set := nil | cons (_:A) (_:list A). \end{coq_example*} This is an alternative definition of lists where we specify the arguments of the constructors rather than their full type. @@ -1036,6 +1036,9 @@ The typical example of a mutual inductive data type is the one for trees and forests. We assume given two types $A$ and $B$ as variables. It can be declared the following way. +\begin{coq_eval} +Reset Initial. +\end{coq_eval} \begin{coq_example*} Variables A B : Set. Inductive tree : Set := |