Stefan Höck

# Steps to Reproduce Run the following: ```idris2 loop : Nat -> PrimIO () loop Z w = MkIORes () w loop (S k) w = let MkIORes () w2...

[ regression ] Package dependencies not resolved correctly

4

I'm afraid #2496 caused another regression with package resolution. The build of today's pack nightly failed with lots of errors. I do realize that we have tested this one or...

Mapping a List over a rank 2 function has O(n^2) time complexity

3

I found the following (reduced to a minimal example) when mapping over the functor wrapped in a free monad: # Steps to Reproduce Run the following program: ```idris mapK :...

[ regression ] Packages with same transitive dependencies no longer build

1

Today I got a couple of mails from GitHub: Most of my packages' nightly builds failed. It looks like their (transitive) dependencies are no longer acceptable to Idris2. For instance:...

[ performance ] More stack safety in the Prelude

2

This PR adds transform rules for making `map`, `mapMaybe`, and `filter` for `List` and `SnocList` plus some other utilities tail recursive. A note about `mapImpl`: The following transform rule is...

Missing syntax

2

This is a non-comprehensive list of syntactic utilities I haven't yet explained in the tutorials. I'll update this whenever something else comes to mind. - [ ] Tuple sections -...