nicolabotta

Great, thanks for providing rmview and for looking into this issue!

I would be happy to try to reproduce the issue on the official app but having upgraded to Debian stable (bullseye) to install rmview I am now unable to install...

Ok, I have managed to run the official windows app under wine on another machine running Debain buster (oldstable). As it turns out, color rendering was broken under `reMarkable-2.11.0.182-win32.exe`: ...

Done: you are right, 2.12.1.187 needs a refresh except when highlighting text which is immediatly rendered in color, sorry for the noise! The only problem I am left with is...

Thanks David, I have opened https://github.com/idris-lang/Idris-dev/issues/4799#issue-543469766. Best, Nicola

As reported in https://github.com/idris-lang/Idris-dev/issues/4799#issuecomment-569899621, there seem to be two problems in the current idris-mode. For syntax highlighting to work as expected for .lidr files, the function ``` (defun idris-highlight-column (idris-col)...

Here is a self-contained example: ``` module issues.FiniteAsInterface import Data.Fin import Data.Vect tail : {0 A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin...

Right, all test were done by running `time idris2 --exec main Linear.idr`. For instance, for `N = 20`: ``` nicola@lt561:~/gitlab/botta/Idris2Libs/tests$ time idris2 --exec main Linear.idr xs(20) = 20 real 0m0.876s...

Hmmm, chez scheme is installed but `:c`does not seem to work as in idris 1: ``` nicola@lt561:~/gitlab/botta/Idris2Libs/tests$ idris2 Linear.idr Welcome to Idris 2 version 0.0. Enjoy yourself! Main> :c linear2.exe...

@chrrasmussen: thanks! I can confirm the problem is a type checking one. Once an executable is generated, the run-time seems to be constant in `N` in idris 2. @edwinb: thanks...