diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-22 21:01:29 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:07 +0100 |
| commit | 899b701462fa056a22f997ae22c5ef7c1d247673 (patch) | |
| tree | ae2e914c7228a10d448afed56db003834b53d28b /doc | |
| parent | 57e66fa78559d76e492ea0f0f2d43086a2f457b6 (diff) | |
Starting revising inductive types session
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 8e1a1766e..5002b905c 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 |