Marek

in idris2 ```idris head_unequal : DecEq a => {1 xs : V n a} -> {1 ys : V n a} -> {x : a} -> {y : _} ->...

thank you for reporting!

This issue is in **Idris 1** and this report duplicates existing issue in Idris1 repository https://github.com/idris-lang/Idris-dev/issues/4433 Good news is that this was fixed in **Idris2** where unique names are generated.

> 1. idris2 executable cannot be found; > Hi @jfdm What is the output when invoking `M-x flycheck-verify-setup` in some *.idr file? > 2. both idris2 and idris flycheckers are...

Over weekend I played with my setup and converted it to use `use-package` which is what I assume 90% users use to install packages. ```elisp (use-package idris-mode ;; :ensure t...

We are getting closer to fix this although there is still some weird behaviour that I don't understand yet. Cold start of Idris2 by loading `test/src/Main.idr` works correctly as at...

> My gut feeling is that Idris2 is more used than Idris1 I would be happy to hear from anyone having real world use cases of Idris1 especially from emacs...

> I wonder if file-name-parent-directory is new for 29.X and we need to be backwards compatible for 27.X and 28.X. Yes, I think we can backport it into `./idris-compat.el` ....

Yes I think so. I havent work with Idris for some time so did quick test now. Loaded few random files in the Idris2 repository itself and everythink worked well...

Hi @jgarte This is good question. I did short exploration few months back on this topic. Seems like we could get similar behaviour using build in `context-menu-mode` feature introduced in...