Andreas Abel
Andreas Abel
Replace record directive `eta-equality` by `no-eta-equality; pattern`. Future Agda might not allow unguarded record types with eta-equality in safe mode anymore. So we switch eta off here, but make the...
From https://agda.zulipchat.com/#narrow/stream/259646-announce/topic/Standard.20library.20v2.2E1/near/455502043 > When will https://agda.github.io/agda-stdlib/v2.1/ be available? NB: Listing the docs under https://agda.github.io/agda-stdlib will probably remain a manual process, but pushing the docs to subfolder _tag_ for a new...
It makes sense to compile abstract definitions to arbitrary Haskell code. (This example is not super clever.) ```agda abstract record Pointer : Set where constructor mkPointer field thePointer : Nat...
Blocked on: - [ ] https://github.com/haskell/cabal/issues/10467 - [x] https://github.com/Lysxia/generic-data/issues/70 - [x] https://github.com/phile314/tasty-silver/issues/45 - [ ] https://github.com/agda/agda/issues/7580
While trying to build Agda with GHC 9.12 (which uses Cabal-3.14): ``` [1 of 2] Compiling Main ( dist-newstyle/build/x86_64-osx/ghc-9.12.20241014/Agda-2.8.0/setup/setup.hs, dist-newstyle/build/x86_64-osx/ghc-9.12.20241014/Agda-2.8.0/setup/Main.o ) dist-newstyle/build/x86_64-osx/ghc-9.12.20241014/Agda-2.8.0/setup/setup.hs:40:37: error: [GHC-83865] • Couldn't match type: [Char] with:...
Commits - **Utils.Lens: add lens and lensProduct, export (&&&)** - **Refactor: SourceFile is FileId instead of AbsolutePath; add FileDict to TCM** Broken tests: - interaction/6194 - lib-interaction/2066 - api-tests/1168 Maybe...
@oskeri and I discovered that artifacts of variable generalization arrive at backends in certain cases, e.g. if you compile `Relation.Nullary.Decidable` of the standard library. Here is the fragment that matters:...
https://github.com/agda/agda/blob/845ebd38f4fc3efe7099c8fcb54c0bfc093d0f6b/src/full/Agda/TypeChecking/Primitive/Cubical.hs#L1267-L1291 @Saizan writes in https://github.com/agda/agda/pull/7534#discussion_r1791350611: > `IntervalUniv` should have the check that's at `SSet` atm. I suppose that got overlooked when `IntervalUniv` got introduced. OTOH it seems then that the...
Left over from - https://github.com/agda/agda/pull/7534#issuecomment-2393789255 @arthur-adjedj wrote: > I have not dived into the issue, but from what I remember, there already were [some known issues](https://github.com/agda/agda/pull/6505#discussion_r1126784433) with regards to mixing...