I am trying to configure Emacs with ProofGeneral (the Coq IDE) to display mathematical symbols in place of the abbreviations ->, =>, forall and exists.

My current .emacs script is as follows:

;; Open .v files with Proof General's Coq mode

(load "~/.emacs.d/lisp/PG/generic/proof-site")

;; Load pretty-mode script

(load "~/.emacs.d/lisp/pretty-mode")

;; Coq symbols

(add-hook 'coq-mode-hook
      (lambda ()
        (mapc (lambda (pair) (push pair prettify-symbols-alist))
            '(("forall". x2200)
              ("->". x2190)
              ("exists". x2203)
              ("=>". x21D2)))))

following examples found here and here.

When I enter coq-mode and enable either or both of global-pretty-mode and global-prettify-symbols-mode, I see no change. I only manage to get a Greek lambda in lisp-mode and python-mode.

Any help would be much appreciated!

  • 1
    x2200 is a symbol with a funny name. Instead you should have a character there. It could be ?∀ or it could be #x2200 or ?\u2200. – Stefan Oct 13 '17 at 20:35

Thanks Stefan for your reply, that solved my issue.

For completeness, I'm posting my full .emacs file in case anybody else is looking to achieve similar formatting results in ProofGeneral:

;; Open .v files with Proof General's Coq mode

(load "~/.emacs.d/lisp/PG/generic/proof-site")

;; Coq symbols

(global-prettify-symbols-mode 1)

(setq coq-symbols-list '(lambda ()
        (mapc (lambda (pair) (push pair prettify-symbols-alist))
            '(("forall". ?∀)
              ("exists". ?∃)
              ("~" . ?¬)
              ("/\\" . ?⋀)
              ("\\/" . ?⋁)
              ("=>". ?⇒)
              ("->". ?→)
              ("<-" . ?←)
              ("<->" . ?↔)
              ("nat" . ?ℕ)
              ("*" . ?×)))))

;; Prettify Coq script editor

(add-hook 'coq-mode-hook coq-symbols-list)

;; Prettify Coq output in proofs
(add-hook 'coq-goals-mode-hook coq-symbols-list)
  • Couple of code suggestions: 1) don't quote lambdas; 2) you can just append your alist to prettify-symbols-alist in one go instead of calling a function for each pair – Basil Oct 14 '17 at 13:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.