coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Implicit arguments/Notations

From: Anthony Bordg <bordg.anthony AT gmail.com>
To: Anthony Bordg <bordg.anthony AT gmail.com>, coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Implicit arguments/Notations
Date: Sat, 25 Feb 2017 21:50:25 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=bordg.anthony AT gmail.com; spf=Pass smtp.mailfrom=bordg.anthony AT gmail.com; spf=None smtp.helo=postmaster AT mail-ot0-f171.google.com
Ironport-phdr: 9a23:ldzJWx/Esr8h9f9uRHKM819IXTAuvvDOBiVQ1KB32ugcTK2v8tzYMVDF4r011RmSDNidsagP0raO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZPebgFIiTanf79+Mhq6oRjeu8UKnIBvNrs/xhzVr3VSZu9Y33loJVWdnxb94se/4ptu+DlOtvwi6sBNT7z0c7w3QrJEAjsmNXs15NDwuhnYUQSP/HocXX4InRdOHgPI8Qv1Xpb1siv9q+p9xCyXNtD4QLwoRTiv6bpgRxj1hicaLD456H/YhdBsjKxVpxKhogZww4/SYIqIMPZzcafQcdYcSGFcXMheSjZBD5u+YIsBD+QPM+VWoZTjqVQSthaxHxWgCfn1xzNUmnP736s32PkhHwHc2wwgGsoDvWjSrNXpNKcSVua1zanVxjjeaPNWwyry6IfVeR0muv6MWqhwftfeyUU1DQzFiEmQqYziPzOT1uUAqGeb7+96WuKuj24rsR1+oj+qxso1jITCm4wbylfB9SpjwYY1I8W1SEF8Yd6jH5tQsz+VO5FqTcMlRmFkoCc6yrscuZ66ZicG0ponxwTHZ/yIcoiI/hLjVPuKLjtimH1lf7e/ihCv+kaj0u3xTsu53VlQoiZYjNXBtmoB2h/N5sSdV/dw/Fqt1DCS3A7J8O5EO1o7la/DJp4h3LEwkp0TvFzGHiDsmUX2iLaadkI4+uS08ujnbKjqq52BO4NuhQH+NaMumsO7AesmKAQBQ2+b+eGk2L3i+032XqlKg+U0n6TWqpzWONoXq66jDwJWzIov8QuzAjW73NgAmHkINlNFeBaJj4jzPFHOJej1Auy4g1S2jThryOrKMafnApXRLnjDl7HhfLZm5k5TzQo819Ff55ZOBr4dJ/LzX1f9tMbEAR8hLwy03+HnBc1h2YMZQGKDG7OWMKfPsVCT/e8vOOmNZIoNuDnnMfQl5vjujWU4mVAHZ6Wp04EXOziEGaFPJVmZZnz9yv0GC2sF9l40S/bmhxuLVyJTYHCjd6057zA/TomhCNGHDouqmfmK2DqxVsldYXkDAVSRG1/pcZ+FUrECcnTBDNVml2ktU6ShTIkwnTuprgP1g+5tKfDY9WsRs47j095kz+LWnBA2szdzCpLOgCm2U2hokzZQFHcN16dlrBkhm1o=

Thanks, the text by Hugo Herbelin seems a good place to start.

2017-02-25 21:31 GMT+01:00 Emilio Jesús Gallego Arias <e AT x80.org>:

Hi Anthony,

Anthony Bordg <bordg.anthony AT gmail.com> writes:

> I would be glad if someone could point out some documentation for the
> mechanisms that handle implicit arguments and notations in Coq.
> I'm looking for something with more details than the reference manual.

If I am not mistaken both are handled at "internalization" time, see
comments in:

https://github.com/coq/coq/blob/trunk/interp/constrintern.mli

You may find more information in some of the presentations of the 2 Coq
implementor workshops, see:

https://coq.inria.fr/cocorico/CoqCodingSprint
https://coq.inria.fr/cocorico/CoqCodingSprint/CoqCS1?action="AttachFile&do=view&target=intro-talk.pdf
https://coq.inria.fr/cocorico/CoqImplementorsWorkshop/CoqIW2016?action="AttachFile&do=view&target=notations.pdf

there may be more resources but I don't remember them right now. Also, I
am pretty sure you can ask specific questions on the coqdev mailing
list.

Best,
Emilio

PhD. Anthony Bordg

postdoctoral fellow

Mathematical Institute Charles University
https://sites.google.com/site/anthonybordg/

[Coq-Club] Implicit arguments/Notations, Anthony Bordg, 02/25/2017
- Re: [Coq-Club] Implicit arguments/Notations, Emilio Jesús Gallego Arias, 02/25/2017
  - Re: [Coq-Club] Implicit arguments/Notations, Anthony Bordg, 02/25/2017