diff options
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 13 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 91 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 43 |
3 files changed, 89 insertions, 58 deletions
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 8e6f85fca3..60b346c211 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -1,7 +1,7 @@ .. _typeclasses: -Type Classes -============ +Typeclasses +=========== This chapter presents a quick reference of the commands related to type classes. For an actual introduction to typeclasses, there is a @@ -150,7 +150,7 @@ To ease the parametrization of developments by typeclasses, one can use the command :cmd:`Context` to introduce variables into section contexts, it works similarly to the :cmd:`Variable` vernacular, except it accepts any binding context as argument, so variables can implicit, and -:ref:`implicit-generalization` can be used (see also :ref:`section-mechanism`). +:ref:`implicit-generalization` can be used. For example: .. coqtop:: all @@ -159,6 +159,8 @@ For example: Context `{EA : EqDec A}. +.. coqtop:: in + Global Program Instance option_eqb : EqDec (option A) := { eqb x y := match x, y with | Some x, Some y => eqb x y @@ -167,6 +169,8 @@ For example: end }. Admit Obligations. +.. coqtop:: all + End EqDec_defs. About option_eqb. @@ -175,6 +179,7 @@ Here the :cmd:`Global` modifier redeclares the instance at the end of the section, once it has been generalized by the context variables it uses. +.. seealso:: Section :ref:`section-mechanism` Building hierarchies -------------------- @@ -280,7 +285,7 @@ Summary of the commands .. cmd:: Class @ident {? @binders} : {? @sort} := {? @ident} { {+; @ident :{? >} @term } } The :cmd:`Class` command is used to declare a typeclass with parameters - ``binders`` and fields the declared record fields. + :token:`binders` and fields the declared record fields. .. _singleton-class: diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index f2d305f4bc..398ad4833d 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -754,49 +754,60 @@ used by ``Function``. A more precise description is given below. Section mechanism ----------------- -The sectioning mechanism can be used to to organize a proof in -structured sections. Then local declarations become available (see -Section :ref:`gallina-definitions`). +Sections create local contexts which can be shared across multiple definitions. +.. example:: -.. cmd:: Section @ident + Sections are opened by the :cmd:`Section` command, and closed by :cmd:`End`. - This command is used to open a section named :token:`ident`. - Section names do not need to be unique. + .. coqtop:: all + Section s1. -.. cmd:: End @ident + Inside a section, local parameters can be introduced using :cmd:`Variable`, + :cmd:`Hypothesis`, or :cmd:`Context` (there are also plural variants for + the former two). - This command closes the section named :token:`ident`. After closing of the - section, the local declarations (variables and local definitions, see :cmd:`Variable`) get - *discharged*, meaning that they stop being visible and that all global - objects defined in the section are generalized with respect to the - variables and local definitions they each depended on in the section. + .. coqtop:: all - .. example:: + Variables x y : nat. - .. coqtop:: all + The command :cmd:`Let` introduces section-wide :ref:`let-in`. These definitions + won't persist when the section is closed, and all persistent definitions which + depend on `y'` will be prefixed with `let y' := y in`. - Section s1. + .. coqtop:: in - Variables x y : nat. + Let y' := y. + Definition x' := S x. + Definition x'' := x' + y'. - Let y' := y. + .. coqtop:: all - Definition x' := S x. + Print x'. + Print x''. - Definition x'' := x' + y'. + End s1. - Print x'. + Print x'. + Print x''. - End s1. + Notice the difference between the value of :g:`x'` and :g:`x''` inside section + :g:`s1` and outside. + +.. cmd:: Section @ident + + This command is used to open a section named :token:`ident`. + Section names do not need to be unique. - Print x'. - Print x''. +.. cmd:: End @ident - Notice the difference between the value of :g:`x'` and :g:`x''` inside section - :g:`s1` and outside. + This command closes the section named :token:`ident`. After closing of the + section, the local declarations (variables and local definitions, see :cmd:`Variable`) get + *discharged*, meaning that they stop being visible and that all global + objects defined in the section are generalized with respect to the + variables and local definitions they each depended on in the section. .. exn:: This is not the last opened section. :undocumented: @@ -808,11 +819,9 @@ Section :ref:`gallina-definitions`). .. cmd:: Variable @ident : @type This command links :token:`type` to the name :token:`ident` in the context of - the current section (see Section :ref:`section-mechanism` for a description of - the section mechanism). When the current section is closed, name :token:`ident` + the current section. When the current section is closed, name :token:`ident` will be unknown and every object using this variable will be explicitly parametrized (the variable is *discharged*). - The :cmd:`Variable` command out of any section is equivalent to :cmd:`Local Parameter`. .. exn:: @ident already exists. :name: @ident already exists. (Variable) @@ -843,7 +852,31 @@ Section :ref:`gallina-definitions`). Context {A : Type} (a b : A). Context `{EqDec A}. - See also :ref:`contexts` in the chapter :ref:`typeclasses`. +.. seealso:: Section :ref:`contexts` in chapter :ref:`typeclasses`. + +.. cmd:: Let @ident := @term + + This command binds the value :token:`term` to the name :token:`ident` in the + environment of the current section. The name :token:`ident` disappears when the + current section is eventually closed, and all persistent definitions and + theorems within the section and depending on :token:`ident` are + prefixed by the let-in definition :n:`let @ident := @term in`. + + .. exn:: @ident already exists. + :name: @ident already exists. (Let) + :undocumented: + + .. cmdv:: Let @ident {? @binders } {? : @type } := @term + :undocumented: + + .. cmdv:: Let Fixpoint @ident @fix_body {* with @fix_body} + :name: Let Fixpoint + :undocumented: + + .. cmdv:: Let CoFixpoint @ident @cofix_body {* with @cofix_body} + :name: Let CoFixpoint + :undocumented: + Module system ------------- diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 1c6fb4b193..67e59768d6 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -634,13 +634,18 @@ has type :token:`type`. Variables {+ ( {+ @ident } : @type ) } Hypothesis {+ ( {+ @ident } : @type ) } Hypotheses {+ ( {+ @ident } : @type ) } - :name: Variable-Parameter; Variables-Parameter; Hypothesis-Parameter; Hypotheses-Parameter + :name: Variable (outside a section); Variables (outside a section); Hypothesis (outside a section); Hypotheses (outside a section) Out of any section, these variants are synonyms of :n:`Local Parameter {+ ( {+ @ident } : @type ) }`. - For their meaning inside a section, see the documentation on + For their meaning inside a section, see :cmd:`Variable` in :ref:`section-mechanism`. + .. warn:: @ident is declared as a local axiom [local-declaration,scope] + + Warning that is emitted when using :cmd:`Variable` instead of + :cmd:`Local Parameter`. + .. note:: It is advised to use the commands :cmd:`Axiom`, :cmd:`Conjecture` and :cmd:`Hypothesis` (and their plural forms) for logical postulates (i.e. when @@ -648,6 +653,8 @@ has type :token:`type`. :cmd:`Parameter` and :cmd:`Variable` (and their plural forms) in other cases (corresponding to the declaration of an abstract mathematical entity). +.. seealso:: Section :ref:`section-mechanism`. + .. _gallina-definitions: Definitions @@ -704,32 +711,18 @@ Section :ref:`typing-rules`. This is equivalent to :cmd:`Definition`. -.. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. - -.. cmd:: Let @ident := @term - - This command binds the value :token:`term` to the name :token:`ident` in the - environment of the current section. The name :token:`ident` disappears when the - current section is eventually closed, and all persistent objects (such - as theorems) defined within the section and depending on :token:`ident` are - prefixed by the let-in definition :n:`let @ident := @term in`. - Using the :cmd:`Let` command out of any section is equivalent to using - :cmd:`Local Definition`. - - .. exn:: @ident already exists. - :name: @ident already exists. (Let) - :undocumented: + .. cmdv:: Let @ident := @term + :name: Let (outside a section) - .. cmdv:: Let @ident {? @binders } {? : @type } := @term - :undocumented: + Out of any section, this variant is a synonym of + :n:`Local Definition @ident := @term`. + For its meaning inside a section, see :cmd:`Let` in + :ref:`section-mechanism`. - .. cmdv:: Let Fixpoint @ident @fix_body {* with @fix_body} - :name: Let Fixpoint - :undocumented: + .. warn:: @ident is declared as a local definition [local-declaration,scope] - .. cmdv:: Let CoFixpoint @ident @cofix_body {* with @cofix_body} - :name: Let CoFixpoint - :undocumented: + Warning that is emitted when using :cmd:`Let` instead of + :cmd:`Local Definition`. .. seealso:: Section :ref:`section-mechanism`, commands :cmd:`Opaque`, :cmd:`Transparent`, and tactic :tacn:`unfold`. |