Wie gebe ich im AGDA-Modus '·' (mittlerer Punkt) ein?

Question

Ich arbeite durch eine paper, die das Mittel-Punkt-Zeichen in Agda-Code verwendet. Ich würde gerne in der Lage sein, es ohne Kopieren/Einfügen zu tippen. Wie kann ich es mit Agda-Modus eingeben?

Ich habe versucht, typische Ressourcen wie

• http://agda.readthedocs.io/en/latest/tools/emacs-mode.html
• http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.UnicodeInput

Answer 1

\cdot gibt Ihnen · und \. gibt Ihnen ∙ (das sind verschiedene Symbole).

Wenn Sie ein Zeichen kopieren/einfügen können, erfahren Sie, wie Sie es eingeben, indem Sie die Option "Agda/Informationen zum Zeichen bei Punkt" im Menü (oder M-x describe-char) auswählen und den Abschnitt to input: betrachten.