G. Allais
G. Allais
> Error: idris2: no bottle available! tells me this is a homebrew error and so should be reported there. As for the build from source, we'd need to know what...
Testing this by running `rm -r build/ && time idris2 --build idris2api.ipkg` on this branch (with `main` merged in) vs `main` and I get a slight slowdown (~5%): ``` main:...
Go for it @CodingCellist! :idrHype:
Nameless modules indeed have this intrinsic ambiguity. But tbh if you're going to document a module, you should probably start by naming it.
Yeah I mean if you're adding documentation to the definitions in a module then it should probably be named. Anonymous ones are only really useful as throwaways to test some...
This is rejected with `%default total` though: > notE is not total, possibly not terminating due to recursive path Main.notE
The current standard practice AFAIK is to cite https://dblp.org/rec/conf/ecoop/Brady21.html
I suppose we could create zotero entries for the releases. I am concerned about making the production of releases even more work though given we've gone more than a year...
Another alternative would be to index the verified version by the raw one. Like so: ```idris public export interface SemigroupV ty (sem : Semigroup ty) where semigroupOpIsAssociative : (l, c,...
"Some difficulties" being that it's unusable to prove anything at all and produces errors impossible to understand. There are actual proofs in the library and the fact that they are...