Unicode-Glyphen für Schlüsselwörter und Operatoren in Coq / Proof General unter Emacs

9

Diese Frage hat mit der Konfiguration des Coq-Modus in Proof General in Emacs zu tun.

Ich versuche, dass Emacs Schlüsselwörter und Notation in Coq automatisch durch die entsprechenden Unicode-Glyphen ersetzt. Es ist mir gelungen, fun als das griechische Kleinbuchstaben Lambda λ zu definieren, forall als das universelle Quantifizierersymbol ∀ usw. Ich hatte keine Probleme Symbole für Wörter zu definieren.

Das Problem ist, dass wenn ich versuche, die Operatoren => , -> , <-> usw. zu ihrem Unicode-Symbol ⇒ → ↔ zu definieren, werden sie nicht durch die entsprechenden Unicode-Glyphen in Coq ersetzt. Sie werden jedoch im *scratch* -Puffer ersetzt, wenn ich sie teste. Ich verwende den gleichen Mechanismus, um Unicode-Glyphen mit der Coq-Notation abzugleichen:

%Vor%

Ich vermute, das Problem ist, dass der Coq-Modus bestimmte Interpunktionszeichen als speziell markiert, also ignoriert Emacs meinen Code, um sie durch die Unicode-Zeichen zu ersetzen, aber ich bin mir nicht sicher. Kann mir bitte jemand etwas dazu sagen?

    
Mayer Goldberg 20.04.2012, 18:14
quelle

1 Antwort

5

Diese Operatoren sind wahrscheinlich Symbole , nicht Wörter , je nach modusspezifischer Syntaxtabelle. Probieren Sie

aus %Vor%     
huaiyuan 21.04.2012, 00:10
quelle