The Coq mailing list

[t x <txrev319 AT gmail.com>]

I know about Notations in Coq.

However, for notation, I can only map one "symbol" at a time.

Suppose I have:

Inductive Pos :=

| One : Pos

| S : Pos -> Pos.

Inductive Int :=

| IZero

| IPos : Pos -> Int

| INeg : Pos -> Int.

Is there a way I can, using only a finite number of lines,  map ..., -3, -2, -1, 0, 1, 2, 3, ... to my own definition of Int?

(or does this require delving down into the level of ocaml)

Thanks!