How to disable my custom notation in Coq?

Question

I've defined a notation to simulate imperative style programming by

Notation "a >> b" := (b a) (at level 50).

However after that, all function-application expression are represented as '>>' style. For example, in proof mode of Coq Toplevel, I can see

bs' : nat >> list

while actually it should be

bs' : list nat

Why does Coq aggressively rewrite all function application styled expression into my customized '>>' representation? How can I restore everything back to normal, I mean I want to see 'a >> b' be interpreted as 'b a' and 'list nat' will not be represented as 'nat >> list'?

Thank you!

Answer 1

By default, Coq assumes that if you define a notation, you want to it for pretty-printing. If you want the notation to never appear in pretty-printing, declare it as “only parsing”.

Notation "a >> b" := (b a) (at level 50, only parsing).

If you want a >> b to be displayed sometimes, you can restrict it to a scope and associate a type to this scope; then the notation will only be applied when the result type is that type.

There's no way to tell Coq “use the notation only where I used it in my source code”, because a term written with a notation is exactly the same as the term written in any other way: the notation used originally is not part of the term.

Answer 2

You could use a definition instead. This way only things you tag as "followedBy" would be reified this way. Otherwise there's no way for the machine to know when to use a space vs. ">>"...

Definition followedBy {A B : Type} (a : A) (b : A -> B) := b a.

Notation "a >> b" := (followedBy a b) (at level 50).