Naïm Camille Favier
Naïm Camille Favier
[Type duality](https://unimath.github.io/agda-unimath/foundation.type-duality.html) talks about a natural transformation between a covariant functor and a contravariant one, which doesn't make sense. We are really talking about the contravariant functor that has the...
After updating to nixpkgs dfb2f12e899db4876308eba6d93455ab7da304cd (Linux 6.16.3, PipeWire 1.4.7) on my Framework Laptop 13 (AMD Ryzen AI 300), the built-in microphone stopped working. Following the advice of the [Arch Linux...
I want autorandr to enable an output with its preferred mode (passing `--preferred` to xrandr). Is there any way to do that? My unsuccessful attempts include setting `mode` to `preferred`,...
Reopens https://github.com/banacorn/agda-mode-vscode/issues/242. In 0.6.4, write the following into `test.lagda.md`: ````agda ```agda module _ where ``` ```` Load the file. Duplicate the `module _ where` line: ````agda ```agda module _ where...
With agda-mode-vscode 0.5.7, if I hit C-c C-l by accident while Agda is already working (e.g. hit C-c C-l twice in rapid succession), the goal numbers get duplicated like this:
Steps to reproduce: 1. Run `pkill agda`. 2. Create an empty file named `foo.agda`, save and load. 3. Create an empty file named `bar.agda`, save and load. 4. Run `pgrep...
**Is your feature request about something that is currently impossible or hard to do? Please describe the problem.** `nix-shell` can be used as a shebang interpreter to make self-contained scripts,...
### Feature description WeeChat uses libc's `wcswidth` implementation, which on my system (using glibc 2.40) incorrectly reports the width of characters like 🅱️ (U+1F171 followed by U+FE0F Variation Selector-16) as...
On 0841987e573249907ab4f9ce1c39b68b93827621: ```agda open import Agda.Builtin.Unit module B (a : ⊤) where record C : Set where field f : ⊤ module X = B tt open B tt using...
...and other small stuff.