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!