Andreas Abel
Andreas Abel
```agda open import Agda.Builtin.Bool open import Agda.Builtin.Equality data D : Set where c : {{ i : true ≡ false }} → D pattern ff = c {{ () }}...
Re #7163: test installing with --enable-executable-dynamic in CI
Andreas & Ulf: Only retry the analysis (`isRigid`) whether it makes sense to check against the target first when there is evidence that it could be successful the next time....
In the long run, cabal build-type `Setup` will be phased out in favor of `Hooks`. The authors of `Hooks` (in development) at WellTyped have provided a patch we can use...
Erik Palmgren's setoid model of type theory at https://github.com/peterlefanulumsdaine/palmgren-archive/tree/main/MLTT-and-setoids checks in around 2.5 minutes in both Agda 2.5.2 and 2.5.3, but starting with 2.5.4 it gets stuck on `V-model-pt6.agda` (which...
Developers need to run `make install-bin` or `make install-deps` first before running goals like `make type-check`. Closes #6262. Pinging developers because this might affect daily dev practice.
Interactive highlighting does not seem to clean up after itself when we have a `λ where`:  Code (not MWE): ```agda open import Agda.Primitive renaming...
```agda module _ (A : Set) where open import Agda.Builtin.Nat open import Agda.Builtin.Sigma data Color : Set where black : Color data Tree' : Color → Nat → Set where...
Re: #4437 Letting computeHead return UnknownHead instead of aborting the injectivity check has the effect that data projections are now classified as injective. Injectivity prevents projection-likeness. Currently, injectivity takes precedence...
As `ubuntu-latest = ubuntu-22.04` is rolled out, - https://github.com/actions/runner-images/issues/6399 our deploy workflow got broken: https://github.com/agda/agda/actions/runs/3603326548/jobs/6071389168 This workflow creates a static binary: ``` args = --disable-executable-profiling --disable-library-profiling --enable-executable-static --enable-split-sections ``` It...