diff options
Diffstat (limited to 'doc/sphinx/language/extensions/arguments-command.rst')
| -rw-r--r-- | doc/sphinx/language/extensions/arguments-command.rst | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst index 0ae9fab7ab..f8c0e23696 100644 --- a/doc/sphinx/language/extensions/arguments-command.rst +++ b/doc/sphinx/language/extensions/arguments-command.rst @@ -86,6 +86,7 @@ Setting properties of a function's arguments the parameter name used in the function definition). Unless `rename` is specified, the list of :n:`@name`\s must be a prefix of the formal parameters, including all implicit arguments. `_` can be used to skip over a formal parameter. + The construct :n:`@name {? % @scope }` declares :n:`@name` as non-implicit if `clear implicits` is specified or at least one other name is declared implicit in the same list of :n:`@name`\s. :token:`scope` can be either a scope name or its delimiting key. See :ref:`binding_to_scope`. `clear implicits` @@ -377,7 +378,7 @@ Effects of :cmd:`Arguments` on unfolding Bidirectionality hints ~~~~~~~~~~~~~~~~~~~~~~ -When type-checking an application, Coq normally does not use information from +When type-checking an application, |Coq| normally does not use information from the context to infer the types of the arguments. It only checks after the fact that the type inferred for the application is coherent with the expected type. Bidirectionality hints make it possible to specify that after type-checking the @@ -394,7 +395,7 @@ the context to help inferring the types of the remaining arguments. * *type inference*, with is inferring the type of a construct by analyzing the construct. Methods that combine these approaches are known as *bidirectional typing*. - Coq normally uses only the first approach to infer the types of arguments, + |Coq| normally uses only the first approach to infer the types of arguments, then later verifies that the inferred type is consistent with the expected type. *Bidirectionality hints* specify to use both methods: after type checking the first arguments of an application (appearing before the `&` in :cmd:`Arguments`), @@ -416,7 +417,7 @@ type check the remaining arguments (in :n:`@arg_specs__2`). Definition b2n (b : bool) := if b then 1 else 0. Coercion b2n : bool >-> nat. - Coq cannot automatically coerce existential statements over ``bool`` to + |Coq| cannot automatically coerce existential statements over ``bool`` to statements over ``nat``, because the need for inserting a coercion is known only from the expected type of a subterm: @@ -431,7 +432,7 @@ type check the remaining arguments (in :n:`@arg_specs__2`). Arguments ex_intro _ _ & _ _. Check (ex_intro _ true _ : exists n : nat, n > 0). -Coq will attempt to produce a term which uses the arguments you +|Coq| will attempt to produce a term which uses the arguments you provided, but in some cases involving Program mode the arguments after the bidirectionality starts may be replaced by convertible but syntactically different terms. |