diff options
author | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-27 14:30:57 +0200 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-27 14:31:35 +0200 |
commit | 2ba1146e0718568fb5adff418e951261a1e693a4 (patch) | |
tree | 06531de235a0cab87d88d05cfd276103dc8eeee5 /doc/sphinx/language | |
parent | bba1fe0ac5deb05f3ade9709a8a044d3d6979368 (diff) |
Improve subsection on mutual inductive types of the Gallina chapter.
Diffstat (limited to 'doc/sphinx/language')
-rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 90 |
1 files changed, 43 insertions, 47 deletions
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 85e4e8e1f..1a8e9a5dc 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -924,71 +924,67 @@ Variants Mutually defined inductive types ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The definition of a block of mutually inductive types has the form: +.. cmdv:: Inductive @ident {? : @type } := {? | } {*| @ident : @type } {* with {? | } {*| @ident {? : @type } } } -.. cmdv:: Inductive @ident : @term := {? | } @ident : @type {* | @ident : @type } {* with @ident : @term := {? | } @ident : @type {* | @ident : @type }} + This variant allows defining a block of mutually inductive types. + It has the same semantics as the above :cmd:`Inductive` definition for each + :token:`ident`. All :token:`ident` are simultaneously added to the environment. + Then well-typing of constructors can be checked. Each one of the :token:`ident` + can be used on its own. -It has the same semantics as the above ``Inductive`` definition for each -:token:`ident` All :token:`ident` are simultaneously added to the environment. -Then well-typing of constructors can be checked. Each one of the :token:`ident` -can be used on its own. + .. cmdv:: Inductive @ident @binders {? : @type } := {? | } {*| @ident : @type } {* with {? | } {*| @ident @binders {? : @type } } } -It is also possible to parametrize these inductive definitions. However, -parameters correspond to a local context in which the whole set of -inductive declarations is done. For this reason, the parameters must be -strictly the same for each inductive types The extended syntax is: + In this variant, the inductive definitions are parametrized + with :token:`binders`. However, parameters correspond to a local context + in which the whole set of inductive declarations is done. For this + reason, the parameters must be strictly the same for each inductive types. -.. cmdv:: Inductive @ident {+ @binder} : @term := {? | } @ident : @type {* | @ident : @type } {* with @ident {+ @binder} : @term := {? | } @ident : @type {* | @ident : @type }} - -The typical example of a mutual inductive data type is the one for trees and -forests. We assume given two types :g:`A` and :g:`B` as variables. It can -be declared the following way. +.. example:: + The typical example of a mutual inductive data type is the one for trees and + forests. We assume given two types :g:`A` and :g:`B` as variables. It can + be declared the following way. -.. coqtop:: in + .. coqtop:: in - Variables A B : Set. + Variables A B : Set. - Inductive tree : Set := - node : A -> forest -> tree + Inductive tree : Set := node : A -> forest -> tree - with forest : Set := - | leaf : B -> forest - | cons : tree -> forest -> forest. + with forest : Set := + | leaf : B -> forest + | cons : tree -> forest -> forest. -This declaration generates automatically six induction principles. They are -respectively called :g:`tree_rec`, :g:`tree_ind`, :g:`tree_rect`, -:g:`forest_rec`, :g:`forest_ind`, :g:`forest_rect`. These ones are not the most -general ones but are just the induction principles corresponding to each -inductive part seen as a single inductive definition. + This declaration generates automatically six induction principles. They are + respectively called :g:`tree_rec`, :g:`tree_ind`, :g:`tree_rect`, + :g:`forest_rec`, :g:`forest_ind`, :g:`forest_rect`. These ones are not the most + general ones but are just the induction principles corresponding to each + inductive part seen as a single inductive definition. -To illustrate this point on our example, we give the types of :g:`tree_rec` -and :g:`forest_rec`. + To illustrate this point on our example, we give the types of :g:`tree_rec` + and :g:`forest_rec`. -.. coqtop:: all - - Check tree_rec. + .. coqtop:: all - Check forest_rec. + Check tree_rec. -Assume we want to parametrize our mutual inductive definitions with the -two type variables :g:`A` and :g:`B`, the declaration should be -done the following way: + Check forest_rec. -.. coqtop:: in + Assume we want to parametrize our mutual inductive definitions with the + two type variables :g:`A` and :g:`B`, the declaration should be + done the following way: - Inductive tree (A B:Set) : Set := - node : A -> forest A B -> tree A B + .. coqtop:: in - with forest (A B:Set) : Set := - | leaf : B -> forest A B - | cons : tree A B -> forest A B -> forest A B. + Inductive tree (A B:Set) : Set := node : A -> forest A B -> tree A B -Assume we define an inductive definition inside a section. When the -section is closed, the variables declared in the section and occurring -free in the declaration are added as parameters to the inductive -definition. + with forest (A B:Set) : Set := + | leaf : B -> forest A B + | cons : tree A B -> forest A B -> forest A B. -See also Section :ref:`section-mechanism`. + Assume we define an inductive definition inside a section + (cf. :ref:`section-mechanism`). When the section is closed, the variables + declared in the section and occurring free in the declaration are added as + parameters to the inductive definition. .. _coinductive-types: |