The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

I was thinking something even stupider than that!  The user gives two 
functions that map between nats and the user type they want to represent 
with number notations:

Inductive mynat : Set := ...

Definition nat2mynat(n : nat) : mynat := ...

Definition mynat2nat(m: mynat) : nat := ...

Declare Nat Syntax mynat Using nat2mynat, mynat2nat : M_scope.

The parser would, whenever it sees a number in the scope M_scope, call 
nat2mynat and use the result.  The printer would, whenever it sees a 
mynat in the scope M_scope, call mynat2nat, and print the resulting number.

-- Jonathan

On 02/21/2016 06:05 PM, Jason Gross wrote:
> I was thinking something stupider: you pass in terms that are treated as
> constructors and required to have the appropriate type signature (a type
> "NAT", an "O : NAT", and an "S : NAT -> NAT" (hopefully the code can be
> parametric over how many universes NAT uses, and whether its polymorphic or
> not, etc), and then notations get translated to applications of S and O,
> and applications of S and O get translated back, and if S and O happen to
> unfold to other things, then unfolding them breaks the notation (which is
> not the end of the world).
> Even better would be to generalize the nat_syntax_plugin to handle things
> like [trunc_index], i.e., things where the base case should be displayed as
> 1 or as -2, etc.
>
> I do not think that we should have to trust Ltac code to get syntax for
> custom natural numbers.
>
> On Sun, Feb 21, 2016 at 5:49 PM, Pierre-Marie Pédrot <
> pierre-marie.pedrot AT inria.fr>
>  wrote:
>
> > On 21/02/2016 23:31, Jason Gross wrote:
> > > How hard would it be to set up the syntax plugins already in Coq so that
> > > they registered vernaculars such as [Declare NatSyntax for nat in
> > > nat_scope [O S].] and similarly for notations for negative numbers,
> > > ascii, strings, etc?
> > Not that difficult, I believe. Yet, we need to rely on a meta-language
> > to pattern-match over terms. Ltac would fit the bill, but I personally
> > find this use a little bit ugly.  The vernacular would probably look like:
> >
> > Parameter myNat : Type.
> >
> > Ltac reify_myNat n :=
> > match n with
> > (* insert a code producing a Z from a myNat here *)
> > end.
> >
> > Declare Nat Syntax myNat reify_myNat.
> >
> > PMP