I'd like to be able to type unicode characters like Π using agda-mode's "\Pi". In Emacs, I used to configure this like:
(load-file (let ((coding-system-for-read 'utf-8)) (shell-command-to-string "agda-mode locate"))) (require 'agda-input); for unicode input via latex names like \forall. (add-hook 'evil-insert-state-entry-hook (lambda () (set-input-method "Agda"))) (add-hook 'evil-insert-state-exit-hook (lambda () (set-input-method nil)))
In Spacemacs, I've enabled the
agda layer (which has nicely found my Homebrew agda installation without addition configuration, thanks). I am able to type "\Pi" in
.agda files an it works. However, it is not available in other modes.