5
Vorrei che, in Coqide, lo stato di prova non usasse una certa notazione (ma usassimo ancora tutte le altre).C'è un modo per disabilitare una notazione specifica in Coq?
È possibile?
A
risposta
0
Da quanto ho capito nella documentazione, non è possibile. Potresti essere in grado di giocare con gli ambiti di apertura/chiusura, ma non sono sicuro che funzionerà, dal momento che si afferma esplicitamente che le notazioni saranno utilizzate per la stampa, quando possibile.
0
Alcuni trucchi che potrebbero essere sufficienti sono descritte qui: How to disable my custom notation in Coq?
Volevo aggiungere puntatore a tale risposta, perché questa domanda arriva prima su Google.
Buona prova, ma questi trucchi non sono sufficienti per fare specificamente ciò che la domanda chiede. – Atsby