coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Implicit arguments/Notations

From: Anthony Bordg <bordg.anthony AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Implicit arguments/Notations
Date: Sat, 25 Feb 2017 19:24:17 +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-f172.google.com
Ironport-phdr: 9a23:bXM8VR8g6e33Xv9uRHKM819IXTAuvvDOBiVQ1KB30+0cTK2v8tzYMVDF4r011RmSDNidsagP0rON+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZPebgFIiTanf79+Mhq6oRjMusQYnIBvNrs/xhzVr3VSZu9Y33loJVWdnxb94se/4ptu+DlOtvwi6sBNT7z0c7w3QrJEAjsmNXs15NDwuhnYUQSP/HocXX4InRdOHgPI8Qv1Xpb1siv9q+p9xCyXNtD4QLwoRTiv6bpgRxj1hicaLD456H/YhdBsjKxVpxKhogZww4/SYIqIMPZzcafQcdYcSGFcXMheSjZBD5u8YYUBDOQPIPhWoJXmqlQUsRezHxOhCP/zxjJKgHL9wK000/4mEQHDxAEtA9QOsGjUrNXyMqcTUf2+wbTPzTXZcvxW1ir25Y/TfRAmu/GDQL1wfdDLxkkpCwPFjlKQqYrlPj6O2eQNtnKU7+tkVe61l2EnrARxryGpy8wxhIfJgYcVxUrF9SV/2Is1Ktq4SEl0Yd6gDpRcrT2VN4xzQs4kXmpmuz46x6UEtJO0ZiQG1Yoryh7FZ/GEbYSE+A/vWeSPLTp+mXlrYqiwhwyo/kil0uD8Vte70FJNriddl9nDrHEN1xjK5siAVvtx4l6t2TiS2w3R9O1IO080la3cK54uxr4/iIAfvljEHi/zgEn2jamWeVs4+uWw6enqba/qqoKCO4J0kA3zMboiltaiDek6LAQCR22b9v691L3n8035WrJKjvgun6bCt5DaP9kUpqGjDwBP1IYj9xa/DzCg0NUYhnQHI1dFdwiGj4jtIV3BPPf4DfKnj1S2jDhr3+zGPqHmApjVMnfDl67hca9h5E5Y1Qo81stS54lUC7EEOPL8QFX9tN3eDh8jMgy72fzrCNtn1tBWZWXaCaiAdajWrFXAsukoOqyHYJIfkDf7MfksofD02ywXg1gYKICvwZsQbmHwNPN8L0rRNXDrmNsOV24Mogo5Sv3Ch1iLUDoVbHG3CfFvrgonAZ6rWN+QDrumh6aMiXvqEw==

Hi,

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.

Best regards

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