coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [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.