Jacques Carette
Jacques Carette
For example: ``` \param x_1 lower x-coordinate: the lower x-coordinate ``` This is completely unhelpful. It would be better to have nothing there rather than repetition. This is true for...
When used for code documentation, it says ``` filename name of the input file: a filepath, absolute or relative, to the file containing the program's inputs ``` which is correct...
PR #4298 reveals that quite often the information that is there is not a definition at all. Even when it is, the definition is not particularly useful. Certainly it is...
This is related to v2.0 and [other's trouble with running the tests](https://github.com/openjournals/joss-reviews/issues/9241). So the released stdlib 2.0 has https://github.com/agda/agda-stdlib/blob/2b8fff10f4033b91a6df4007e4a65cb10047c89c/src/System/Directory/Primitive.agda#L29 whereas released stdlib 2.1 has https://github.com/agda/agda-stdlib/blob/039e1f4abda49f307f7ed1f5e15232a1c8e9c48c/src/System/Directory/Primitive.agda#L29 `git blame` says that this...
One reviewer writes: > The installation instructions are too general, ideally I would like to see a list of dependencies and the exact version requirement for a particular release. I...
Here is a minimal example of the ills that we get with `--cubical-compatible` that we don't with `--without-K`: ```agda {-# OPTIONS --cubical-compatible --safe #-} module MWE where open import Data.Nat.Base...
Reasoning combinators for monoid, renamed and adapted for Ring. Builds on #2692 .