The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

Unimath defines a small number of notations in their Preamble.v. Any 
other numbers are not covered.

Notation  "0" := (O) : nat_scope.
Notation  "1" := (S 0) : nat_scope.
Notation  "2" := (S 1) : nat_scope.
Notation  "3" := (S 2) : nat_scope.
Notation  "4" := (S 3) : nat_scope.
Notation  "5" := (S 4) : nat_scope.
Notation  "6" := (S 5) : nat_scope.
Notation  "7" := (S 6) : nat_scope.
Notation  "8" := (S 7) : nat_scope.
Notation  "9" := (S 8) : nat_scope.
Notation "10" := (S 9) : nat_scope.
Notation "11" := (S 10) : nat_scope.
Notation "12" := (S 11) : nat_scope.
Notation "13" := (S 12) : nat_scope.
Notation "14" := (S 13) : nat_scope.
Notation "15" := (S 14) : nat_scope.
Notation "16" := (S 15) : nat_scope.
Notation "17" := (S 16) : nat_scope.
Notation "18" := (S 17) : nat_scope.
Notation "19" := (S 18) : nat_scope.
Notation "20" := (S 19) : nat_scope.
Notation "21" := (S 20) : nat_scope.
Notation "22" := (S 21) : nat_scope.
Notation "23" := (S 22) : nat_scope.
Notation "24" := (S 23) : nat_scope.
Notation "100" := (10 * 10) : nat_scope.
Notation "1000" := (10 * 100) : nat_scope.


Gaëtan Gilbert

On 14/05/2018 16:31, José Manuel Rodriguez Caballero wrote:
>     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 
> <mailto: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
>  
> <mailto: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
>         <https://maps.google.com/?q=Am+Campeon+10&entry=gmail&source=g>-12,
>         85579 Neubiberg, Germany
>         Tel: +49 89 99 8853-0, www.intel.de <http://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