Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Pretty-printing numbers


Chronological Thread 
  • From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Pretty-printing numbers
  • Date: Sat, 11 Oct 2014 19:47:09 -0400

On 10/11/2014 07:03 PM, Nikita Karetnikov wrote:
But how exactly Coq does that?
It has been implemented as a plugin written in OCaml, see

plugins/syntax/nat_syntax.ml

in the Coq source tree.

Is it possible with a user-defined type (e.g., binary numbers)?
Yes, but not in a nice modular way. You can just copy/paste the file mentioned above, and make it work with your own number type.

However, for the binary naturals (the types positive, N, and Z) from the standard library, Coq already has built in syntax support in the same way as for nat.



Archive powered by MHonArc 2.6.18.

Top of Page