coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Nikita Karetnikov <nikita AT karetnikov.org>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Pretty-printing numbers
- Date: Sun, 12 Oct 2014 03:03:45 +0400
“Because natural numbers are such a pervasive form of data, Coq provides
a tiny bit of built-in magic for parsing and printing them: ordinary
arabic numerals can be used as an alternative to the "unary" notation
defined by the constructors S and O.” [1]
But how exactly Coq does that? Is it possible with a user-defined type
(e.g., binary numbers)?
[1] https://www.cis.upenn.edu/~bcpierce/sf/current/Basics.html
Attachment:
pgp9Grw60BFWN.pgp
Description: PGP signature
- [Coq-Club] Pretty-printing numbers, Nikita Karetnikov, 10/12/2014
- Re: [Coq-Club] Pretty-printing numbers, Robbert Krebbers, 10/12/2014
- Re: [Coq-Club] Pretty-printing numbers, Arthur Azevedo de Amorim, 10/12/2014
- Re: [Coq-Club] Pretty-printing numbers, Robbert Krebbers, 10/12/2014
Archive powered by MHonArc 2.6.18.