Naïm Camille Favier
Naïm Camille Favier
Fixes https://github.com/plt-amy/1lab/issues/407 and another similar bug. This is still in the spirit of using `overlapOk` as a heuristic for "we now have a list of 'good enough' candidates that would...
Minimised from https://github.com/the1lab/1lab/pull/427#discussion_r1732698143 ```agda open import Agda.Builtin.Nat open import Agda.Builtin.Equality data _≤_ : Nat → Nat → Set where 0≤x : ∀ {x} → 0 ≤ x s≤s : ∀...
While fixing https://github.com/plt-amy/1lab/issues/405, I found another seemingly unrelated bug with irrelevant instance metas: with the current Agda master, the module ```agda open import 1Lab.Type open import 1Lab.HLevel open import 1Lab.HLevel.Closure...
Some people are complaining that the HoTT book uses $\mathsf{max}(x, y)$ to denote the $\mathsf{sup}$ operation in a lattice, and in particular the $\mathsf{sup}$ of two real numbers, whereas in...
```agda {- {- -} {! !} -} _ = {! !} ``` The hole is created in the first line instead of the second line. (Heh, GitHub's parser is also...
**Have you read the [FAQ](https://github.com/RetroMusicPlayer/RetroMusicPlayer/blob/master/FAQ.md)?** Yes **Has the bug already been reported? Please search in GitHub issue tab before creating an issue.** No **Describe the bug** A [song](https://jamiepaige.bandcamp.com/album/women-wrestling) titled 🤼♀️...
### Feature description Terminals encode key chords like alt+w as an escape character (`ESC`, `\x1B`) followed by `w`. As a result, pressing the Escape key followed by w has the...
I seem to recall that drawing two parallel arrows between the same nodes would result in them automatically being offset evenly, but at some point that changed. It now looks...
Follows up and replaces https://github.com/agda/agda/pull/7818 Adds a build flag that controls whether the data directory is under XDG_DATA_HOME (the default) or in its standard location (which makes more sense for...
Things like `**$(o, \ell)$-complete**` (from [this page](https://1lab.dev/Cat.Diagram.Limit.Base.html#completeness)) are [transformed](https://github.com/the1lab/1lab/blob/aafcd46dd4d4cff3bfff260a2decb067d61531ad/support/shake/app/Shake/Markdown.hs#L111-L117) to something like `**$(o, \ell)\textnormal{-complete}$**`, which loses the boldness information. Maybe we could walk `Inline`s, keeping track of when we encounter...