Skip to content

Instantly share code, notes, and snippets.

@L-TChen

L-TChen/agda-input-emacs.MD

Created July 27, 2020 11:47
Show Gist options
  • Star 4 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save L-TChen/dc86f1d220125c636d37b7c2b294d1e3 to your computer and use it in GitHub Desktop.
Save L-TChen/dc86f1d220125c636d37b7c2b294d1e3 to your computer and use it in GitHub Desktop.
Download ZIP
Go to definitions in Agda mode combined with Evil mode in Emacs
Raw
agda-input-emacs.MD

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)
@quomat
Copy link

quomat commented Dec 31, 2023

Thank you a ton! I tried global-unset-key but it couldn't work ;(

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment