Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Pretty-printing numbers

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Pretty-printing numbers


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.18.

Top of Page