Come disabilitare la mia notazione personalizzata in Coq?

Question

ho definito una notazione per simulare la programmazione imperativa stile da

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

Tuttavia dopo che, ogni espressione funzione di applicazione sono rappresentati come '>>' stile. Ad esempio, in modalità di prova di Coq Toplevel, posso vedere

bs' : nat >> list 

, mentre in realtà dovrebbe essere

bs' : list nat 

Perché Coq aggressivamente riscrivere tutte le applicazioni funzione espressione nel mio stile personalizzato '>>' rappresentazione? Come posso ripristinare tutto alla normalità, voglio dire che voglio vedere 'a >> b' essere interpretato come 'b a' e 'list nat' non sarà rappresentato come 'nat >> list'?

Grazie!

Answer 1

Per impostazione predefinita, Coq presuppone che se si definisce una notazione, vuoi per pretty-printing . Se si desidera che la notazione non appaia mai nella stampa carina, dichiararla come "solo parsing".

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

Se si desidera a >> b da visualizzare a volte, si può limitare a un campo di applicazione e di associare un tipo a questo scopo; quindi la notazione verrà applicata solo quando il tipo di risultato è quel tipo.

Non c'è modo di dire a Coq "usa la notazione solo dove l'ho usato nel mio codice sorgente", perché un termine scritto con una notazione è esattamente lo stesso del termine scritto in altro modo: la notazione usata in origine è non parte del termine.

Answer 2

È possibile utilizzare una definizione. In questo modo solo le cose che taggate come "followBy" verrebbero reificate in questo modo. In caso contrario, non c'è modo per la macchina di sapere quando usare uno vs spazio ">>" ...

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

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