From 50af46a596af607493ce46da782389e8a82e8354 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 18 Nov 2020 23:25:17 +0100 Subject: [attributes] [doc] Documentation review by Théo. Co-authored-by: --- doc/sphinx/language/core/coinductive.rst | 3 ++- doc/sphinx/language/core/definitions.rst | 8 +++++--- doc/sphinx/language/core/inductive.rst | 10 ++++++---- 3 files changed, 13 insertions(+), 8 deletions(-) (limited to 'doc/sphinx/language') diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst index 43bbc8b40d..e9737f8712 100644 --- a/doc/sphinx/language/core/coinductive.rst +++ b/doc/sphinx/language/core/coinductive.rst @@ -27,7 +27,8 @@ More information on co-inductive definitions can be found in This command supports the :attr:`universes(polymorphic)`, :attr:`universes(template)`, :attr:`universes(cumulative)`, - :attr:`private(matching)`, and :attr:`using` attributes. + :attr:`private(matching)`, :attr:`typing(universes)`, + :attr:`typing(positive)`, and :attr:`using` attributes. .. example:: diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index 57771c9036..95bb1b0e0c 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -90,8 +90,9 @@ Section :ref:`typing-rules`. computation on :n:`@term`. These commands also support the :attr:`universes(polymorphic)`, - :attr:`program` (see :ref:`program_definition`), - :attr:`canonical` and :attr:`using` attributes. + :attr:`program` (see :ref:`program_definition`), :attr:`canonical`, + :attr:`typing(universes)`, :attr:`typing(guarded)`, and + :attr:`using` attributes. If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. @@ -162,7 +163,8 @@ Chapter :ref:`Tactics`. The basic assertion command is: correct at some time of the interactive development of a proof, use the command :cmd:`Guarded`. - This command accepts the :attr:`using` attribute. + This command accepts the :attr:`typing(universes)`, + :attr:`typing(guarded)`, and :attr:`using` attributes. .. exn:: The term @term has type @type which should be Set, Prop or Type. :undocumented: diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index f277997094..86de059f28 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -32,7 +32,8 @@ Inductive types This command supports the :attr:`universes(polymorphic)`, :attr:`universes(template)`, :attr:`universes(cumulative)`, - :attr:`typing(positive)`, and :attr:`private(matching)` attributes. + :attr:`typing(positive)`, :attr:`typing(universes)`, and + :attr:`private(matching)` attributes. Mutually inductive types can be defined by including multiple :n:`@inductive_definition`\s. The :n:`@ident`\s are simultaneously added to the environment before the types of constructors are checked. @@ -51,8 +52,8 @@ Inductive types The types of the constructors have to satisfy a *positivity condition* (see Section :ref:`positivity`). This condition - ensures the soundness of the inductive definition. The - positivity checking can be disabled using the :flag:`Positivity + ensures the soundness of the inductive definition. + Positivity checking can be disabled using the :flag:`Positivity Checking` flag or the :attr:`typing(positive)` attribute (see :ref:`controlling-typing-flags`). @@ -392,7 +393,8 @@ constructions. consequently :n:`forall {* @binder }, @type` and its value is equivalent to :n:`fun {* @binder } => @term`. - This command accepts the :attr:`program` attribute. + This command accepts the :attr:`program`, + :attr:`typing(universes)`, and :attr:`typing(guarded)` attributes. To be accepted, a :cmd:`Fixpoint` definition has to satisfy syntactical constraints on a special argument called the decreasing argument. They -- cgit v1.2.3