Stefan Höck

This is expected behavior. Idris, unlike JavaScript, uses euclidian modulo. See the discussion here: #1048 and #1480.

OK. Sorry about that. I'll submit a fix.

According to the tests we run, `%` works fine. So, according to your Edit: Can we use the operator or not? I'm afraid your messages are often rather cryptic...

Quick update: If I use an explicit erased argument, the program runs instantaneously. ```idris mapK : {0 f,g : _} -> ((0 x : Type) -> f x -> g...

Personally, I think the Idris2 project should at least keep supporting those parts of contrib that also make an appearance in the compiler, such as lexing, parsing, and pretty printing...

We have to be *very* careful about this, as it looks like it shows quadratic runtime complexity due to #2166. For instance, if I run the following program on my...

Two more data points: The following, which uses a trick described in #2166 by using a function with an explicit erased argument, does not work here: ```idris foldlDImpl : (0...

OK, I got a O(n) version without `believe_me` by using a helper function for the recursion: ```idris foldlD : (0 accTy : Nat -> Type) -> (f : forall k....

This is strange. Any idea why the windows test fails?

Actually, I forgot the correctness proof for `SnocList`s tail recursive append, and indeed, the implementation was wrong. :-)