Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] implicit arguments

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] implicit arguments


Chronological Thread 
  • From: Fabian Kunze <fabian.kunze AT cs.uni-saarland.de>
  • To: Jeremy Dawson <coq-club AT inria.fr>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] implicit arguments
  • Date: Sun, 13 Dec 2020 08:39:34 +0000 (UTC)
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=fabian.kunze AT cs.uni-saarland.de; spf=Pass smtp.mailfrom=fabian.kunze AT cs.uni-saarland.de; spf=None smtp.helo=postmaster AT thyone.hiz-saarland.de
  • Ironport-phdr: 9a23:e7BgrBL9Kf4/b9uzCdmcpTZWNBhigK39O0sv0rFitYgfKPvxwZ3uMQTl6Ol3ixeRBMOHsq0C0rqL+Pm5CSQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagY75+Ngi6oAbRu8UZnIduN6U8wQbVr3VVfOhb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQLJBFDgpPHw768PttRnYUAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4btnRAPuhSwaMTMy7WPZhdFqjK9DrhyvpwJxzY3Wb4GbKfRxcb/Sc9wBSGpdR8ZcTTBNDp+gY4YNCecKIOZWr5P6p1sLtRawBROjC/juyjBSgH/9wKg00/knEQDHwgMrAtUDsHrOo9ruNacdS+a1wLPLzTXeafNX2Cny5ZPUfRA6u/2MQLRwccvIxUk0DQzKlE+QqYj/MDOTy+sBqXWU4PR5WO+plmUopB1/rCK1yccwlonGmJgVylbc+Cllz4g4JN22RFB1bNOkFJZetyKXOYV3T888Q29lpjo2x7IJt5C1YSUExpAqyh/RZvKIfYaF7BztWemNLDp7mX9ofq+0iRi18Uil0OL8V8+03U5LripDiNnMt2oC2wbd6sidTPZ240Sv2S6X2gzO5OxJLlo4mK7aJpI7wLM8jIQfvErdEiPum0j7jrWaelgn9+Wn8ejrf7frq5uGO4Nplw3zMqIjkdGlD+siKAgBRW2b9Py81LL9+U35R61HjuE2kqjZt5DaI9oUqrS5Aw9U04cv8g2/AC2839QCmXkINlRFdw+dg4f0JV7COPH4DfGhjFSwiDpn2v7LM7L7DpjJL3XPirXscaxj50NS1gY/1dVf6IhVCrEFLvLzQEjxtNnAAx83KQO72OfnB8971o8EWmKPH6mZMaLMvlKT+u0vOPOAZJITuDb8MvQl/OThgmUjmV8ZZ6ap24YYZGqlEft4O0mZe2bjgs8dEWcWuQozVPDliFqbUTJKe3myW7886SogBYK9DYbDQ5itj6ab0Ce6GJ1WfGFGBUqWHXfmbYXXE8sLPQCfOMJkg3QoXKe6TIlpgRqprUrxz6dtBuvS4CwR85z5gotb/erWwD87/z19CYy+zmefQikgkGoCRjYwmqNip15w4lyYl7V+grlDHNVJ4/pPXkE2OMiPnKRBF9nuV1eZLZ+yQ1G8T4D+WG1jfpcK29YLJn1FNZC6lBmZh3ihGPkIkb3OH5U96KbV2XS3K8svky+bhplktEEvR450DUPjhqN78FKPVZLJgkKfmuCqdLZZxyfE7mOKy2bIsEwKCFchA5WAZmgWYw7tlfq840rDS7G0DrF9allK0oifLKoPcdTgl1FPQvulNNmMOm8=

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
>>



Archive powered by MHonArc 2.6.19+.

Top of Page