diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 8e1a1766e5..5002b905c7 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -534,11 +534,11 @@ reductions or any combination of those can also be defined. \section[Inductive Definitions]{Inductive Definitions\label{Cic-inductive-definitions}} A (possibly mutual) inductive definition is specified by giving the -names and the type of the inductive sets or families to be -defined and the names and types of the constructors of the inductive -predicates. An inductive declaration in the global environment can -consequently be represented with two local contexts (one for inductive -definitions, one for constructors). +names and types of the inductive types to be +defined and the names and types of the constructors of the inductive types. +An inductive declaration in the global environment can +consequently be represented with two local contexts, one for the types +one for the constructors. Stating the rules for inductive definitions in their general form needs quite tedious definitions. We shall try to give a concrete |