G. Allais
G. Allais
[A list of the currently existing commands](https://agda.readthedocs.io/en/latest/tools/emacs-mode.html) First, two commands which are similar enough to others that it shouldn't be to awful to add them: * `C-c C-z` takes a...
I was reading an issue on the Idris bug tracker where people were puzzled by the use of "strictly positive". Given that we have great documentation covering these topics ([case...
This one is hard to reproduce: * the fact `_Preserves_⟶_` is defined via `_on_` is crucial * the fact `length` is defined via `fold` is crucial `cong` and `cong'` have...
Still missing: CHANGELOG entries
Currently http://agda.github.io/agda-stdlib/Text.Pretty.html suffers from various limitations: 1. Performance: [`__`](http://agda.github.io/agda-stdlib/Text.Pretty.html#2508) only filters the invalid results, it does not discard the dominated ones. This doesn't prevent combinatorial explosion (we've been experiencing issues...
In `Data.List.Properties` we have: ```agda unfold-reverse : ∀ (x : A) xs → reverse (x ∷ xs) ≡ reverse xs ∷ʳ x ʳ++-defn : ∀ (xs : List A) {ys}...
Cf. [this blog post](https://doisinkidney.com/posts/2018-12-21-balancing-scans.html) by @oisdk > We’re not using the proofs in Agda’s standard library because these are tied to propositional equality. In other words, instead of using an...
Should we add an `Algebra.Structures.Literals` module declaring a `Number` instance for any `SemiringWithoutAnnihilatingZero` interpreting `n` as `1 + ... + 1`?
In #1123 we are talking about a breaking change to a module that was just released. Hence the question: should we add a user warning to new modules telling people...
In `Data.Integer.Properties`, ```agda pos-distrib-* : ∀ x y → (+ x) * (+ y) ≡ + (x ℕ* y) ``` is the symmetric of the *not yet existing* function ```agda...