The Coq mailing list

[Arnaud Spiwack <Arnaud.Spiwack AT lix.polytechnique.fr>]

Hi,

There is no such way, unfortunately. It's been wanted for a long time, 
but no one came up with a convincing design for such a feature.

Currently, all such notations are hacked into the OCaml source of Coq. 
It's neither satisfying, nor elegant.

You'll have to resort to coercions in your case, I guess.


Arnaud Spiwack

Andrew McCreight a écrit :
> Hello,
>
> Is there some way to declare my own custom interpretation of integer 
> constants in a scope, as are available in the nat and Z scopes?  If I 
> have a function Z_to_foo : Z -> foo, I'd like to be able to make, for 
> instance, "4" automatically intepreted as "Z_to_foo 4" in a particular 
> context.  I looked around on the manual and the nat and Z libraries 
> but couldn't find anything.  Coercions sort of do what I want, but it 
> doesn't seem like you can tie them to particular notation scopes.  Or 
> is this how nat and Z do it?  Thanks!
>
> -Andrew
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club