The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

Hi Fabian,

Info on which implicit arguments are inferred and inserted.

For example, in my example below, what rule determines the type of 
no_rpt_same seq_ord (prems:=prems)

In general, f x (y := z) is equivalent to
what (eg @f _ _ x _ _ z _ _ ....)?

I do see that the question is answered in part, in the middle of the 
document you point to, which is mostly about which arguments are 
implicit, so it is easy to miss if you are looking for info about when 
implicit arguments are inserted.  But that part of the question is what 
I refer to below where I say "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)"

Do you know whether that information is in the document you point to (or 
anywhere else for that matter)?

Jeremy

On 13/12/20 7:39 pm, Fabian Kunze wrote:
> 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