The Coq mailing list

[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