coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: e AT x80.org (Emilio Jesús Gallego Arias)
To: Anthony Bordg <bordg.anthony AT gmail.com>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Implicit arguments/Notations
Date: Sat, 25 Feb 2017 21:31:08 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Neutral smtp.mailfrom=e AT x80.org; spf=None smtp.helo=postmaster AT cc-tupan-roaming-b.ensmp.fr
Ironport-phdr: 9a23:X5yvPh8r1pNpU/9uRHKM819IXTAuvvDOBiVQ1KB90uMcTK2v8tzYMVDF4r011RmSDNidsagP0rGJ++C4ACpbvsbH6ChDOLV3FDY7yuwu1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9Dq3PF4XTl8W60fyps92WOl0QxWn1XbQnBROqrQLXp4E8hpFuJe5lwBzTrnQOcuJKxWRuNHqcmh/94oG7+5s1oApKvPd0+uZQAf28eL43Bfx1CTUiMmd9xsDwJwKLYgKL4nYTVS0/iBtBGEmWv1nBQp7tv36i5aJG0y6AMJizFOhsVA==
Organization: X80 Heavy Industries

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

[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