The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

FYI, there is on-going work to make this more uniform and allow easily extending the types which support such "numeral" notation (see https://github.com/coq/coq/pull/496).

Théo

Le lun. 14 mai 2018 à 12:10, Soegtrop, Michael <michael.soegtrop AT intel.com> a écrit :

Dear Gergely,

SF defines its own nats in a module NatPlayground and then closes this module, so that the standard library nats are used. They do the same trick several times to just explain how things are done but then go back to the library definitions.

The nat notation is pretty hard wired into Coq. In Init.Datatypes at the beginning you find:

Declare ML Module "nat_syntax_plugin".

(note: this is not shown in the HTML dumps of the library sources, you need to look into the .v file). Afaik this does the trick. I can't tell how the nat type is actually connected to this plugin, I think it is simply hard wired by name in the plugin.

I guess this is nothing the Coq community is especially proud of, but it did work so far ...

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928