diff options
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 31 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 62 |
2 files changed, 55 insertions, 38 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index f474eade71..a93e9b156d 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -148,7 +148,7 @@ available: It can be activated for printing with -.. cmd:: Set Printing Projections. +.. opt:: Printing Projections .. example:: @@ -249,7 +249,7 @@ printing of pattern-matching over primitive records. Primitive Record Types ++++++++++++++++++++++ -When the ``Set Primitive Projections`` option is on, definitions of +When the :opt:`Primitive Projections` option is on, definitions of record types change meaning. When a type is declared with primitive projections, its :g:`match` construct is disabled (see :ref:`primitive_projections` though). To eliminate the (co-)inductive type, one must use its defined primitive projections. @@ -328,7 +328,7 @@ patterns are allowed, as in ML-like languages. The extension just acts as a macro that is expanded during parsing into a sequence of match on simple patterns. Especially, a construction defined using the extended match is generally printed -under its expanded form (see ``Set Printing Matching`` in :ref:`controlling-match-pp`). +under its expanded form (see :opt:`Printing Matching`). See also: :ref:`extendedpatternmatching`. @@ -874,7 +874,7 @@ In the syntax of module application, the ! prefix indicates that any Starts an interactive module satisfying each `module_type`. - .. cmdv:: Module @ident {* @module_binding} <: {+<; @module_type }. + .. cmdv:: Module @ident {* @module_binding} <: {+<: @module_type }. Starts an interactive functor with parameters given by the list of `module_binding`. The output module type is verified against each `module_type`. @@ -955,7 +955,8 @@ Reserved commands inside an interactive module type: is a shortcut for the command ``Include`` `module` for each `module`. -.. cmd:: @assumption_keyword Inline @assums. +.. cmd:: @assumption_keyword Inline @assums + :name: Inline The instance of this assumption will be automatically expanded at functor application, except when this functor application is prefixed by a ``!`` annotation. @@ -1435,7 +1436,9 @@ For instance, the first argument of in module ``List.v`` is strict because :g:`list` is an inductive type and :g:`A` will always be inferable from the type :g:`list A` of the third argument of -:g:`cons`. On the contrary, the second argument of a term of type +:g:`cons`. Also, the first argument of :g:`cons` is strict with respect to the second one, +since the first argument is exactly the type of the second argument. +On the contrary, the second argument of a term of type :: forall P:nat->Prop, forall n:nat, P n -> ex nat P @@ -1506,10 +1509,10 @@ inserted. In the second case, the function is considered to be implicitly applied to the implicit arguments it is waiting for: one says that the implicit argument is maximally inserted. -Each implicit argument can be declared to have to be inserted -maximally or non maximally. This can be governed argument per argument -by the command ``Implicit Arguments`` (see Section :ref:`declare-implicit-args`) or globally by the -command ``Set Maximal Implicit Insertion`` (see Section :ref:`controlling-insertion-implicit-args`). +Each implicit argument can be declared to have to be inserted maximally or non +maximally. This can be governed argument per argument by the command ``Implicit +Arguments`` (see Section :ref:`declare-implicit-args`) or globally by the +:opt:`Maximal Implicit Insertion` option. See also :ref:`displaying-implicit-args`. @@ -1882,7 +1885,7 @@ arguments that are not detected as strict implicit arguments. This “defensive” mode can quickly make the display cumbersome so this can be deactivated by turning this option off. -See also: ``Set Printing All`` in :ref:`printing_constructions_full`. +See also: :opt:`Printing All`. Interaction with subtyping ~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2134,9 +2137,9 @@ sensitive to the implicit arguments). Turning this option on deactivates all high-level printing features such as coercions, implicit arguments, returned type of pattern-matching, notations and various syntactic sugar for pattern-matching or record projections. -Otherwise said, ``Set Printing All`` includes the effects of the commands -``Set Printing Implicit``, ``Set Printing Coercions``, ``Set Printing Synth``, -``Unset Printing Projections``, and ``Unset Printing Notations``. To reactivate +Otherwise said, :opt:`Printing All` includes the effects of the options +:opt:`Printing Implicit`, :opt:`Printing Coercions`, :opt:`Printing Synth`, +:opt:`Printing Projections`, and :opt:`Printing Notations`. To reactivate the high-level printing features, use the command ``Unset Printing All``. .. _printing-universes: diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 246f45b3e7..a9c4dd7588 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -557,9 +557,10 @@ has type :token:`type`. the global context. The fact asserted by *term* is thus assumed as a postulate. -.. exn:: @ident already exists +.. exn:: @ident already exists (Axiom) .. cmdv:: Parameter @ident : @term. + :name: Parameter Is equivalent to ``Axiom`` :token:`ident` : :token:`term` @@ -582,6 +583,7 @@ has type :token:`type`. qualified name to refer to them. .. cmdv:: Conjecture @ident : @term + :name: Conjecture Is equivalent to ``Axiom`` :token:`ident` : :token:`term`. @@ -594,7 +596,7 @@ will be unknown and every object using this variable will be explicitly parametrized (the variable is *discharged*). Using the ``Variable`` command out of any section is equivalent to using ``Local Parameter``. -.. exn:: @ident already exists +.. exn:: @ident already exists (Variable) .. cmdv:: Variable {+ @ident } : @term. @@ -607,6 +609,7 @@ of any section is equivalent to using ``Local Parameter``. .. cmdv:: Variables {+ ( {+ @ident } : @term) }. .. cmdv:: Hypothesis {+ ( {+ @ident } : @term) }. + :name: Hypothesis .. cmdv:: Hypotheses {+ ( {+ @ident } : @term) }. @@ -643,7 +646,7 @@ Section :ref:`typing-rules`. This command binds :token:`term` to the name :token:`ident` in the environment, provided that :token:`term` is well-typed. -.. exn:: @ident already exists +.. exn:: @ident already exists (Definition) .. cmdv:: Definition @ident : @term := @term. @@ -687,7 +690,7 @@ prefixed by the let-in definition ``let`` :token:`ident` ``:=`` :token:`term` ``in``. Using the ``Let`` command out of any section is equivalent to using ``Local Definition``. -.. exn:: @ident already exists +.. exn:: @ident already exists (Let) .. cmdv:: Let @ident : @term := @term. @@ -1245,20 +1248,25 @@ the theorem is bound to the name :token:`ident` in the environment. .. exn:: The term @term has type @type which should be Set, Prop or Type -.. exn:: @ident already exists +.. exn:: @ident already exists (Theorem) The name you provided is already defined. You have then to choose another name. .. cmdv:: Lemma @ident : @type. + :name: Lemma .. cmdv:: Remark @ident : @type. + :name: Remark .. cmdv:: Fact @ident : @type. + :name: Fact .. cmdv:: Corollary @ident : @type. + :name: Corollary .. cmdv:: Proposition @ident : @type. + :name: Proposition These commands are synonyms of ``Theorem`` :token:`ident` : :token:`type`. @@ -1273,16 +1281,16 @@ the theorem is bound to the name :token:`ident` in the environment. coinduction has to be done is assumed to be non ambiguous and is guessed by the system. - Like in a ``Fixpoint`` or ``CoFixpoint`` definition, the induction hypotheses - have to be used on *structurally smaller* arguments (for a ``Fixpoint``) or - be *guarded by a constructor* (for a ``CoFixpoint``). The verification that + Like in a :cmd:`Fixpoint` or :cmd:`CoFixpoint` definition, the induction hypotheses + have to be used on *structurally smaller* arguments (for a :cmd:`Fixpoint`) or + be *guarded by a constructor* (for a :cmd:`CoFixpoint`). The verification that recursive proof arguments are correct is done only at the time of registering the lemma in the environment. To know if the use of induction hypotheses is correct at some time of the interactive development of a proof, use the command :cmd:`Guarded`. - The command can be used also with ``Lemma``, ``Remark``, etc. instead of - ``Theorem``. + The command can be used also with :cmd:`Lemma`, :cmd:`Remark`, etc. instead of + :cmd:`Theorem`. .. cmdv:: Definition @ident : @type. @@ -1313,16 +1321,20 @@ the theorem is bound to the name :token:`ident` in the environment. This generalizes the syntax of CoFixpoint so that one or more bodies can be defined interactively using the proof editing mode. -.. cmd:: Proof. … Qed. +.. cmd:: Proof -A proof starts by the keyword Proof. Then Coq enters the proof editing mode -until the proof is completed. The proof editing mode essentially contains -tactics that are described in chapter :ref:`Tactics`. Besides tactics, there are -commands to manage the proof editing mode. They are described in Chapter -:ref:`proofhandling`. When the proof is completed it should be validated and -put in the environment using the keyword Qed. + A proof starts by the keyword Proof. Then Coq enters the proof editing mode + until the proof is completed. The proof editing mode essentially contains + tactics that are described in chapter :ref:`Tactics`. Besides tactics, there + are commands to manage the proof editing mode. They are described in Chapter + :ref:`proofhandling`. -.. exn:: @ident already exists +.. cmd:: Qed + + When the proof is completed it should be validated and put in the environment + using the keyword Qed. + +.. exn:: @ident already exists (Qed) .. note:: @@ -1341,14 +1353,16 @@ put in the environment using the keyword Qed. realizing some form of *proof-irrelevance*. To be able to unfold a proof, the proof should be ended by Defined (see below). -.. cmdv:: Proof. … Defined. +.. cmdv:: Defined + :name: Defined - Same as ``Proof. … Qed.`` but the proof is then declared transparent, - which means that its content can be explicitly used for - type-checking and that it can be unfolded in conversion tactics - (see :ref:`performingcomputations`, :cmd:`Opaque`, :cmd:`Transparent`). + Same as :cmd:`Qed` but the proof is then declared transparent, which means + that its content can be explicitly used for type-checking and that it can be + unfolded in conversion tactics (see :ref:`performingcomputations`, + :cmd:`Opaque`, :cmd:`Transparent`). -.. cmdv:: Proof. … Admitted. +.. cmdv:: Admitted. + :name: Admitted Turns the current asserted statement into an axiom and exits the proof mode. |