The Coq mailing list

[Fabian Kunze <fabian.kunze AT cs.uni-saarland.de>]

Dear Jeremy,
What are you missing from 
https://coq.inria.fr/distrib/current/refman/language/extensions/implicit-arguments.html
?
In the beginning the page explains all the different kinds of reasons 
argument could be made implicit (or better, how some arguments could be 
inferred in use), and then the optons/flags are listed which enable/disable 
the detection/declaration of those kinds of implicit arguments when defining 
new constants.

What more would you expect to be explained there?

Best,
Fabian

12 Dec 2020 12:42:51 Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>:

> Hi Jim,
> 
> Thanks.  I think the second reference was meant to be
> https://coq.inria.fr/distrib/current/refman/language/core/definitions.html#grammar-token-term_let
> but that is for a different use of :=
> 
> I've found a section on := used as in this case, it's at
> https://coq.inria.fr/distrib/current/refman/language/extensions/implicit-arguments.html
> under the heading Explicit applications
> but it doesn't include info on when implicit argments are implicitly 
> inserted
> 
> Whereabouts can I find information about what is happening here?
> 
> Thanks,
> 
> Jeremy
> 
> On 10/12/20 3:32 pm, Jim Fehrle wrote:
>> 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 
>> <mailto: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
>>