The Coq mailing list

[José Manuel Rodriguez Caballero <josephcmac AT gmail.com>]

Gergely Buday said
in Software Foundations' first file, Basics.v, the file defines
Inductive nat : Type :=
  | O : nat
  | S : nat -> nat.
and then, magically, uses decimal numerals, 3, 5 and so on for it.

This is not the case when you work with the library UniMath. For example,

When I write "Eval compute in  2 + 2" I obtain the answer "= 4: nat". But when I write "Eval compute in  2 + 222" I obtain the answer "Error: No interpretation for numeral 222".

2018-05-14 16:24 GMT+02:00 Théo Zimmermann <theo.zimmi AT gmail.com>:

I don't think there are anything planned for strings yet but feel free to open a feature request if you think that would be valuable ;-)

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

Dear Théo,

 

Interesting! One question: is there also something planned for quoted character strings? These are also somehow “magically” converted to Coq string objects. It might be interesting to convert strings to arbitrary objects with a parsing function depending on scope in a similar way as numbers are converted in the PR you mentioned. E.g. the Software Foundations “ImpParser.v” shows how to parse strings with simple programs to data structures. Since Menhir can generate Coq parsers (Afaik) this might be a powerful feature.

 

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