G. Allais
G. Allais
Manual (but documented in the release guide)
If you are often inserting the same arguments, you may want to declare a pattern synonym for the more explicit constructor.
Similar issue with the emptyness check not seeing through `abstract` / `opaque` blocks. I can see arguments going either ways: why should it be possible to rely on this potentially...
We had the proof in the original PR thread: #450
I'm happy for it to be closed but there may still be further instances.
> We could define `≤-total` in terms of `_≤?_` and `≰⇒≥`, but this requires some annoying reordering of `Data.Nat.Properties`. I think that was the suggestion, and I think it's worth...
I would be strongly against `-fast` suffixes: the fast version should IMO be the default and we can have a `-spec` variant for the equivalent but more proof-friendly version.
Ah sorry, I originally labeled it a refactoring before re-labeling it a *performance* bug and removing the refactoring label. I had not noticed you had added it back and so...
I've installed [git-sizer](https://github.com/github/git-sizer/) and it points at 8a02d2470d553f70042a8a99fa3641e724e9635e being the biggest commit (100M). This is indeed a haddock commit. The `docs/` directory on `gh-pages` is a whooping 150M when all...
> I considered this, but don't have enough space to install a new PL. It was available on the debian repos, I did not need to compile it myself.