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: Jim Fehrle <jim.fehrle AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] implicit arguments
  • Date: Sat, 12 Dec 2020 23:19:00 -0800
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jim.fehrle AT gmail.com; spf=Pass smtp.mailfrom=jim.fehrle AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f180.google.com
  • Ironport-phdr: 9a23:aENCeB/9cz7WHf9uRHKM819IXTAuvvDOBiVQ1KB20u8cTK2v8tzYMVDF4r011RmVBNqdsqIZwLSG+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxhKiTanfL9/LxW7oQrQu8QVnIBvNrs/xhzVr3VSZu9Y33loJVWdnxb94se/4ptu+DlOtvwi6sBNT7z0c7w3QrJEAjsmNXs15NDwuhnYUQSP/HocXX4InRdOHgPI8Qv1Xpb1siv9q+p9xCyXNtD4QLwoRTiv6bpgRRn1gykFKjE56nnahcN+jK1ZoByvqR9xzZPKbo6JL/dxZL/RcMkASGZdQspcVSpMCZ68YYsVCOoBOP5VoY38p1sLsBCwBRejBOP1yj9MmHD9wKo30+YgEQHDxgAgEcwBsHTOrNXxKqgfSu+1zKzSwjXCa/Nawyvy6I/Nch04p/yHQL1/f9bLx0Y1CwPFkkufqZbjPz6N1+kDvGmW4u5vWO6zhWAqtwJ8ryayy8syloTEh4IYx1HH+Ch5wIg7KtK2RFB7b9OlEZZcqz+WOpZ2T88+XW1ltyA3waAIt568eSgF0pUnxxjHZvyIcoiI/hLjVPuKLjtinn5qZLW/hxOq/Uivy+38Ssm00EtRoSZfjtbMsXUN2wTO5ciGUfty4kCh2SuV1wDI9O5IO080lbDcK5482r48jpsSsVnHHi/3gEX5kK+WeV84+uSy9+vnZbDmq5mBPIF3kgHzKroiltC7DOgiMQUDX3KX9fm92bDi50H1XbZHguEwn6LEqp7VP94bqbS8AwJN0oYs9RK/DzC+3dQdh3YHLVZFdAuGj4jtJl3COf74Aeq8jliwijtryPfGPrruApXJMHfPiqvufbF460JEyQozy85Q545MB70fPP7+XlX9ud/YAxMjLgC5wufqBM9g2o4dRW6DGqqZP7nTsV+M6OIvOe6MZIoNtTb/Kvgl4uTijXEnll8dZ6mp2YUYZWu3HvRjOUqZYH7sjs0dHmcNuwoyVPbqh0GaUT5Pe3ayWLox6S08CIK/FIvMWoStgKGa0yqgBZ1XZmVGCkiWHnvydoWEXe0MaCOILcN7nDwET+vpd4h03ha38QT+1rBPL+zO+yReu4iw+sJy4rjxlBR62zF0FcCQmzWPTmQykG4IXTs79K96qE15jFyE1P4r0LRjCdVP6qYRAU8BPpnGwrkiUo2gakf6Zt6MDW2ebJCmDDU2FIxjxtYPZwN8H4zngEmTh2ylBLgak7HND5sxoPqFjirBYv1lwnOD75EPylwvQ89BL2qj3/ct+A3aBoqPmEKcxf/zKfYsmRXV/WLG9lKg+VlCWVcpA6rAVHEbIEDRqIah6w==

Hi Jeremy,

If you're really stuck on syntax, try this:  The full grammar from which the documentation is generated is here: https://github.com/coq/coq/blob/master/doc/tools/docgram/orderedGrammar.  Find the nonterminal you need, then search the `.rst` files in the source tree for `<nonterminal_name> ::=` to find its definition.  Each .rst generates an html file with the same prefix.  The html path is based on the rst file path.  Note that the syntax has not yet been updated in some chapters, notably the tactics and SSR chapters.

Let me know if you find orderedGrammar useful; we've debated whether it should be included as an appendix.

For implicits, you might also try posting on https://coq.discourse.group/ or asking on https://coq.zulipchat.com/.  I don't know the feature well enough to answer your question.

Jim



Archive powered by MHonArc 2.6.19+.

Top of Page