diff options
Diffstat (limited to 'doc/sphinx/language/extensions')
| -rw-r--r-- | doc/sphinx/language/extensions/arguments-command.rst | 16 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/canonical.rst | 4 |
2 files changed, 17 insertions, 3 deletions
diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst index 2460461ede..d178311b4c 100644 --- a/doc/sphinx/language/extensions/arguments-command.rst +++ b/doc/sphinx/language/extensions/arguments-command.rst @@ -79,7 +79,7 @@ Setting properties of a function's arguments `!` the function will be unfolded only if all the arguments marked with `!` - evaulate to constructors. See :ref:`Args_effect_on_unfolding`. + evaluate to constructors. See :ref:`Args_effect_on_unfolding`. :n:`@name {? % @scope }` a *formal parameter* of the function :n:`@reference` (i.e. @@ -89,11 +89,25 @@ Setting properties of a function's arguments 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`. + .. exn:: To rename arguments the 'rename' flag must be specified. + :undocumented: + + .. exn:: Flag 'rename' expected to rename @name into @name. + :undocumented: + `clear implicits` makes all implicit arguments into explicit arguments + + .. exn:: The 'clear implicits' flag must be omitted if implicit annotations are given. + :undocumented: + `default implicits` automatically determine the implicit arguments of the object. See :ref:`auto_decl_implicit_args`. + + .. exn:: The 'default implicits' flag is incompatible with implicit annotations. + :undocumented: + `rename` rename implicit arguments for the object. See the example :ref:`here <renaming_implicit_arguments>`. `assert` diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst index f7ce7f1c6c..aa754ab63d 100644 --- a/doc/sphinx/language/extensions/canonical.rst +++ b/doc/sphinx/language/extensions/canonical.rst @@ -490,10 +490,10 @@ We need some infrastructure for that. Definition id {T} {t : T} (x : phantom t) := x. Notation "[find v | t1 ~ t2 ] p" := (fun v (_ : unify t1 t2 None) => p) - (at level 50, v ident, only parsing). + (at level 50, v name, only parsing). Notation "[find v | t1 ~ t2 | s ] p" := (fun v (_ : unify t1 t2 (Some s)) => p) - (at level 50, v ident, only parsing). + (at level 50, v name, only parsing). Notation "'Error : t : s" := (unify _ t (Some s)) (at level 50, format "''Error' : t : s"). |