4

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!

ryan221b
  • 151
  • 5
  • 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

1 Answers1

1

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)
ryan221b
  • 151
  • 5
  • 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