Skip to content

Instantly share code, notes, and snippets.

@L-TChen
L-TChen / agda-input-emacs.MD
Created July 27, 2020 11:47
Go to definitions in Agda mode combined with Evil mode in Emacs

Evil mode overwrites the mouse-2 event which is used by Agda to go to the definition of clicked identifier. To restore the desired behavioru, just add the following line after enabling Evil (require 'evil)

(define-key evil-normal-state-map [mouse-2] 'agda2-goto-definition-mouse)