The Coq mailing list

[Jim Fehrle <jim.fehrle AT gmail.com>]

Check this section of the manual: https://coq.inria.fr/distrib/current/refman/language/extensions/arguments-command.html, that may have what you seek.  Still lots of things in the manual need improvement.

However, I'm not an expert on implicit arguments.

It's a bit hard to index :=, it's used in 77 places in the grammar.  A few non-alphabetic items appear in the general index, but what's there is probably woefully inadequate.  Here is one basic use:

http://localhost:63342/coq2/doc/sphinx/_build/html/language/core/definitions.html#grammar-token-term_let

Jim

On Wed, Dec 9, 2020 at 7:46 PM Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> wrote:

Hi,

I have tried to find out when implicit arguments are inserted.  Is this
in the documentation anywhere?

With a function

lja_dd_ord < About no_rpt_same.
no_rpt_same :
forall U : Type,
relationT U ->
forall (rules : list U -> U -> Type) (prems : U -> Type) (c0 : U),
derrec rules prems c0 -> Type

Arguments U, rules, prems, c0 are implicit

I find

lja_dd_ord < Check no_rpt_same seq_ord.
no_rpt_same seq_ord
      : forall (rules : list (srseq (PropF ?V)) -> srseq (PropF ?V) -> Type)
          (prems0 : srseq (PropF ?V) -> Type) (c0 : srseq (PropF ?V)),
        derrec rules prems0 c0 -> Type

which is as I expected (as a matter of fact, I can't find this
documented either, but I've discovered from experience that implicit
arguments (non-maximal) are inserted up to the last explicit argument)

but

lja_dd_ord < Check no_rpt_same seq_ord (prems:=prems).
no_rpt_same seq_ord (prems:=prems)
      : forall c0 : srseq (PropF V), derrec ?rules prems c0 -> Type

ie it seems to have inserted the implicit argument rules also.

What are the rules about this?

And if there are any tips for finding things like this in the
documentation, I'd appreciate it.  For example, the symbol := isn't in
the general index, which I would have expected.

Thanks

Jeremy