G. Allais
G. Allais
There's an open PR for the backport I still need to fix when I'll have time
I find it a lot easier to push documentation following *specific* demands for clarification rather than abstract calls to actions. Otherwise I am overwhelmed by the possibilities and don't really...
To clarify: :+1: on the second part; I don't have any opinion wrt org-mode vs. basic comments.
It feels wrong to use #613 to justify coming to a decision in #595 when #595 was used to justify coming to a decision in #613. Now that README/ has...
> Also: `Codata.Sized.Delay` and friends? We indeed have e.g. https://agda.github.io/agda-stdlib/v2.2/Effect.Monad.Partiality.html
TIL. Still, if the implicit argument was not named in the `data` definition then it does not show up in the goal and there is no way to introduce it...
Once we have these docstrings clearly attached to specific definitions, we can use them to improve discovery via `C-c C-z` by allowing users to look for terms in docs.
As a rule of thumb, it's always good to match on the view rather than the expression (i.e. on the `IsValue` proof directly)
We'll need to bump some dependencies given we're using a newer GHC, a newer Agda, etc. We'll also need to modify the `run` of the new test cases added since...
Alright, it now successfully builds on my machine. Let's see if CI agrees :)