G. Allais
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...