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!
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.
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).
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With