Jak wyłączyć niestandardową notację w Coq?

Question

Mam zdefiniowane notacji symulować programowania imperatyw styl przez

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

Jednak po tym wszystkim ekspresja funkcja-aplikacji są reprezentowane jako „>>” stylu. Na przykład, w trybie Dowód Coq Toplevel widzę

bs' : nat >> list 

podczas gdy w rzeczywistości powinno być

bs' : list nat 

Dlaczego Coq agresywnie przepisać cały aplikacji funkcja stylem ekspresji do mojego dostosowane „>>” reprezentacja? Jak mogę przywrócić wszystko do normalności, to znaczy chcę, aby "a >> b" było interpretowane jako "b a", a "lista nat" nie będzie reprezentowana jako "lista nat"?

Dziękujemy!

Answer 1

Domyślnie Coq zakłada, że ​​jeśli zdefiniować notacji, chcesz go do ładnego drukowania . Jeśli chcesz, aby notacja nigdy nie pojawiała się w ładnym druku, zadeklaruj ją jako "tylko parsującą".

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

Jeśli chcesz a >> b być wyświetlane czasami można ograniczyć go do zakresu i skojarzyć typ do tego zakresu; wtedy notacja zostanie zastosowana tylko wtedy, gdy typ wyniku jest tego typu.

Nie ma sposobu, aby powiedzieć Coqowi: "używaj notacji tylko tam, gdzie użyłem jej w moim kodzie źródłowym", ponieważ termin zapisany z notacją jest dokładnie taki sam jak termin zapisany w jakikolwiek inny sposób: pierwotnie używana notacja jest nie jest częścią tego terminu.

Answer 2

Zamiast tego można użyć definicji. W ten sposób tylko reszta oznaczona jako "followBy" zostanie w ten sposób naprawiona. W przeciwnym razie nie ma mowy o maszyna wiedzieć kiedy użyć Vs. kosmiczny „>>” ...

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

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