G. Allais

It's on purpose that the `papers/` library is not installed with the other ones as it's not meant to be reusable content but rather propaganda / complex constructions taken from...

> (2) faster! — saves 15-20% for idris2.rkt / 75-85% for hello.rkt (ymmv) Faster to compile or to run?

Sorry I don't have the headspace for that atm, I'm trying to get #1990 mergd first. I'm happy to see a racket build come back, it's only turned off because...

This issue is about splitting off `contrib` into parts that are meant to be included in `base` and separate packages maintained by the community. Let us please not debate the...

I don't think it's a bug: to cast an integer to a `Fin` you *do* need to be able to inspect that `n` at runtime. https://github.com/idris-lang/Idris2/blob/f58a96e420a8cfbbce7eefbe22581c99cc10c6e7/libs/base/Data/Fin.idr#L216-L218 It just happens to...

What happens if you match on, say, `Yes (Refl {x = S k})` or `Yes (Refl {x = n})`?

If you don't add any defining equation for `nonZeroNatIsSucc`, you get an error indicating that (probably because of the overloading) Idris does not bind `k` because it cannot figure out...

If we're going to expose the internals, then I'd rather we use the [`foldl`-based implementation](http://agda.github.io/agda-stdlib/Data.Vec.Base.html#8726) than this one with a lot of rewriting.

I suppose this should ideally be fixed in the unelaboration pass. Because this won't catch with-apps on the RHS for instance!

> I don't understand the case. With-apps on the RHS are coded with IWithApp and are showed correctly. Oh really? So it's strange we're failing to do it on the...