Holes in Agda are a good bit more powerful than in Haskell, and agda's emacs mode has a bunch of very powerful commands for working with them, eg: listing possi

Holes in Agda are a good bit more powerful than in Haskell, and agda's emacs mode has a bunch of very powerful commands for working with them, eg: listing possible values, automatically filling, splitting them by case, etc. For example, for this post's "jonk" example I just had to copy the type into emacs, reformat it a bit into Agda syntax, then press C-c C-a and it automatically figured out the solution that the author worked through manually: λ z z₁ z₂ → z₁ (λ z₃ → z₂ (z z₃)) See the full list of commands at https://agda.readthedocs.io/en/v2.5.2/tools/emacs-mode.html https://agda.readthedocs.io/en/v2.5.2/tools/emacs-mode.html