diff options
Diffstat (limited to 'doc/sphinx/language/extensions/arguments-command.rst')
| -rw-r--r-- | doc/sphinx/language/extensions/arguments-command.rst | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst index 29877e1b32..2460461ede 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` @@ -181,7 +182,7 @@ Manual declaration of implicit arguments Automatic declaration of implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - The ":n:`default implicits`" :token:`args_modifier` clause tells |Coq| to automatically determine the + The ":n:`default implicits`" :token:`args_modifier` clause tells Coq to automatically determine the implicit arguments of the object. Auto-detection is governed by flags specifying whether strict, @@ -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. |