<commit_before>.. _ArgumentsCommand:

Setting properties of a function's arguments
++++++++++++++++++++++++++++++++++++++++++++

.. cmd:: Arguments @reference {* @arg_specs } {* , {* @implicits_alt } } {? : {+, @args_modifier } }
   :name: Arguments

   .. insertprodn argument_spec args_modifier

   .. prodn::
      argument_spec ::= {? ! } @name {? % @scope_key }
      arg_specs ::= @argument_spec
      | /
      | &
      | ( {+ @argument_spec } ) {? % @scope_key }
      | [ {+ @argument_spec } ] {? % @scope_key }
      | %{ {+ @argument_spec } %} {? % @scope_key }
      implicits_alt ::= @name
      | [ {+ @name } ]
      | %{ {+ @name } %}
      args_modifier ::= simpl nomatch
      | simpl never
      | default implicits
      | clear implicits
      | clear scopes
      | clear bidirectionality hint
      | rename
      | assert
      | extra scopes
      | clear scopes and implicits
      | clear implicits and scopes

   Specifies properties of the arguments of a function after the function has already
   been defined.  It gives fine-grained
   control over the elaboration process (i.e. the translation of Gallina language
   extensions into the core language used by the kernel).  The command's effects include:

   * Making arguments implicit. Afterward, implicit arguments
     must be omitted in any expression that applies :token:`reference`.
   * Declaring that some arguments of a given function should
     be interpreted in a given scope.
   * Affecting when the :tacn:`simpl` and :tacn:`cbn` tactics unfold the function.
     See :ref:`Args_effect_on_unfolding`.
   * Providing bidirectionality hints.  See :ref:`bidirectionality_hints`.

   This command supports the :attr:`local` and :attr:`global` attributes.
   Default behavior is to limit the effect to the current section but also to
   extend their effect outside the current module or library file.
   Applying :attr:`local` limits the effect of the command to the current module if
   it's not in a section.  Applying :attr:`global` within a section extends the
   effect outside the current sections and current module in which the command appears.

      `/`
         the function will be unfolded only if it's applied to at least the
         arguments appearing before the `/`.  See :ref:`Args_effect_on_unfolding`.

         .. exn:: The / modifier may only occur once.
            :undocumented:

      `&`
         tells the type checking algorithm to first type check the arguments
         before the `&` and then to propagate information from that typing context
         to type check the remaining arguments. See :ref:`bidirectionality_hints`.

         .. exn:: The & modifier may only occur once.
            :undocumented:

      :n:`( ... ) {? % @scope }`
         :n:`(@name__1 @name__2 ...)%@scope` is shorthand for :n:`@name__1%@scope @name__2%@scope ...`

      :n:`[ ... ] {? % @scope }`
         declares the enclosed names as implicit, non-maximally inserted.
         :n:`[@name__1 @name__2 ... ]%@scope` is equivalent to :n:`[@name__1]%@scope [@name__2]%@scope ...`

      :n:`%{ ... %} {? % @scope }`
         declares the enclosed names as implicit, maximally inserted.
         :n:`%{@name__1 @name__2 ... %}%@scope` is equivalent to :n:`%{@name__1%}%@scope %{@name__2%}%@scope ...`

      `!`
         the function will be unfolded only if all the arguments marked with `!`
         evaulate to constructors.  See :ref:`Args_effect_on_unfolding`.

      :n:`@name {? % @scope }`
         a *formal parameter* of the function :n:`@reference` (i.e.
         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.
         :token:`scope` can be either a scope name or its delimiting key.  See :ref:`binding_to_scope`.

      `clear implicits`
         makes all implicit arguments into explicit arguments
      `default implicits`
         automatically determine the implicit arguments of the object.
         See :ref:`auto_decl_implicit_args`.
      `rename`
         rename implicit arguments for the object.  See the example :ref:`here <renaming_implicit_arguments>`.
      `assert`
         assert that the object has the expected number of arguments with the
         expected names.  See the example here: :ref:`renaming_implicit_arguments`.

         .. warn:: This command is just asserting the names of arguments of @qualid. If this is what you want, add ': assert' to silence the warning. If you want to clear implicit arguments, add ': clear implicits'. If you want to clear notation scopes, add ': clear scopes'
            :undocumented:

      `clear scopes`
         clears argument scopes of :n:`@reference`
      `extra scopes`
         defines extra argument scopes, to be used in case of coercion to ``Funclass``<commit_msg>Doc: added "Arguments" removing implicit arguments<commit_after>.. _ArgumentsCommand:

Setting properties of a function's arguments
++++++++++++++++++++++++++++++++++++++++++++

.. cmd:: Arguments @reference {* @arg_specs } {* , {* @implicits_alt } } {? : {+, @args_modifier } }
   :name: Arguments

   .. insertprodn argument_spec args_modifier

   .. prodn::
      argument_spec ::= {? ! } @name {? % @scope_key }
      arg_specs ::= @argument_spec
      | /
      | &
      | ( {+ @argument_spec } ) {? % @scope_key }
      | [ {+ @argument_spec } ] {? % @scope_key }
      | %{ {+ @argument_spec } %} {? % @scope_key }
      implicits_alt ::= @name
      | [ {+ @name } ]
      | %{ {+ @name } %}
      args_modifier ::= simpl nomatch
      | simpl never
      | default implicits
      | clear implicits
      | clear scopes
      | clear bidirectionality hint
      | rename
      | assert
      | extra scopes
      | clear scopes and implicits
      | clear implicits and scopes

   Specifies properties of the arguments of a function after the function has already
   been defined.  It gives fine-grained
   control over the elaboration process (i.e. the translation of Gallina language
   extensions into the core language used by the kernel).  The command's effects include:

   * Making arguments implicit. Afterward, implicit arguments
     must be omitted in any expression that applies :token:`reference`.
   * Declaring that some arguments of a given function should
     be interpreted in a given scope.
   * Affecting when the :tacn:`simpl` and :tacn:`cbn` tactics unfold the function.
     See :ref:`Args_effect_on_unfolding`.
   * Providing bidirectionality hints.  See :ref:`bidirectionality_hints`.

   This command supports the :attr:`local` and :attr:`global` attributes.
   Default behavior is to limit the effect to the current section but also to
   extend their effect outside the current module or library file.
   Applying :attr:`local` limits the effect of the command to the current module if
   it's not in a section.  Applying :attr:`global` within a section extends the
   effect outside the current sections and current module in which the command appears.

      `/`
         the function will be unfolded only if it's applied to at least the
         arguments appearing before the `/`.  See :ref:`Args_effect_on_unfolding`.

         .. exn:: The / modifier may only occur once.
            :undocumented:

      `&`
         tells the type checking algorithm to first type check the arguments
         before the `&` and then to propagate information from that typing context
         to type check the remaining arguments. See :ref:`bidirectionality_hints`.

         .. exn:: The & modifier may only occur once.
            :undocumented:

      :n:`( ... ) {? % @scope }`
         :n:`(@name__1 @name__2 ...)%@scope` is shorthand for :n:`@name__1%@scope @name__2%@scope ...`

      :n:`[ ... ] {? % @scope }`
         declares the enclosed names as implicit, non-maximally inserted.
         :n:`[@name__1 @name__2 ... ]%@scope` is equivalent to :n:`[@name__1]%@scope [@name__2]%@scope ...`

      :n:`%{ ... %} {? % @scope }`
         declares the enclosed names as implicit, maximally inserted.
         :n:`%{@name__1 @name__2 ... %}%@scope` is equivalent to :n:`%{@name__1%}%@scope %{@name__2%}%@scope ...`

      `!`
         the function will be unfolded only if all the arguments marked with `!`
         evaulate to constructors.  See :ref:`Args_effect_on_unfolding`.

      :n:`@name {? % @scope }`
         a *formal parameter* of the function :n:`@reference` (i.e.
         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.
         This declares the name as non-implicit if either `clear implicits` is declared 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`
         makes all implicit arguments into explicit arguments
      `default implicits`
         automatically determine the implicit arguments of the object.
         See :ref:`auto_decl_implicit_args`.
      `rename`
         rename implicit arguments for the object.  See the example :ref:`here <renaming_implicit_arguments>`.
      `assert`
         assert that the object has the expected number of arguments with the
         expected names.  See the example here: :ref:`renaming_implicit_arguments`.

         .. warn:: This command is just asserting the names of arguments of @qualid. If this is what you want, add ': assert' to silence the warning. If you want to clear implicit arguments, add ': clear implicits'. If you want to clear notation scopes, add ': clear scopes'
            :undocumented:

      `clear scopes`
         clears argument scopes of :n:`@reference`
      `extra scopes`
         defines extra argument scopes, to be used in case of coercion to ``Funclass``
{'fraction_non_alphanumeric': 0.10863344844597927, 'fraction_numerical': 0.0023680315737543167, 'mean_word_length': 2.775046554934823, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5558286', 'n_tokens_mistral': 2902, 'n_tokens_neox': 2771, 'n_words': 1087}