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.


Adding the hooks to the dotspacemacs/user-config function seems work.

(defun dotspacemacs/user-config ()
  "Configuration function for user code.
This function is called at the very end of Spacemacs initialization after
layers configuration.
This is the place where most of your configurations should be done. Unless it is
explicitly specified that a variable should be set before a package is loaded,
you should place your code here."
  (add-hook 'evil-insert-state-entry-hook (lambda () (set-input-method "Agda")))
  (add-hook 'evil-insert-state-exit-hook (lambda () (set-input-method nil)))

Let me know if there's a better way.

  • If this resolves the problem, please accept your own answer so we can mark the question as answered.
    – Dan
    Oct 7 '17 at 15:10
  • 1
    I am not using spacemacs but this solution worked for me. I had to add (require 'agda-input) before the two add-hook lines though.
    – space junk
    Nov 29 '19 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.