Andreas Abel

I second the addition to examples to the library. Each (file) module could have a (file) submodule `.Example` explaining the use of the primitives. Usually, when adding new functionality to...

Deafening silence.

We could turn of all identifier highlighting for `_` but would that be an improvement?

OP is still open.

There is the `arch` condition, maybe that could be used: https://cabal.readthedocs.io/en/3.14/cabal-package-description-file.html#conditions ``` if os(darwin) && arch(aarch64) ```

```agda {-# OPTIONS -v interaction.case:30 #-} open import Agda.Primitive levelOf : ∀ {a} {A : Set a} → A → Level levelOf a = {!a₁!} -- C-c C-c ``` ```...

Confirmed (e.g. for `ansi-terminal`). ``` ansi-terminal $ cabal-3.16.0.0 repl Resolving dependencies... ``` Previously there was an internal error: ``` ansi-terminal $ cabal-3.14.2.0 repl Configuration is affected by the following files:...

@ulysses4ever wrote: > When I run cabal with -v3 it gives away the stdin it provides curl with: > > ``` > --anyauth > --user ArtemPelenitsyn: > ``` The `--anyauth`...

> weird NotLeqLevel errors for Set1 and Set (lsuc lzero) Here is the evidence: https://github.com/agda/agda/actions/runs/16851129315/job/47737858171#step:9:71 > Issue1724.agda:75.13-17: error: [NotLeqSort] > Set₁ is not less or equal than > Set (Agda.Primitive.lsuc...

The issue can be triggered with making `--double-check` fail hard on errors such as `NotLeqSort`, see PR: - #8061 Failing hard is what `--double-check` should do, I think, because we...