mechvel
mechvel
Thanks to people for the explanation. The code by James is not type-checked, for several reasons. I modify it this way: ```agda import Data.List.Relation.Binary.Pointwise as ListPoint open import Data.Nat using...
Andreas wrote > Using Setoid a (a ⊔ ℓ) instead of Setoid a ℓ restricts uses to situation where the type of the equality relation is at least as b...
James wrote "... as for extensions also to other algebraic structures, that's why I opened issue #2767 to track this specific use case. As for iterating List in order to...
> It is not true that factorisation is always to primes, only into factors (~ divisors). For example, a valid factorisation of 24 > could be 4 times 6, even...
On 2025-09-03 15:15, jwaldmann wrote: > jwaldmann left a comment (agda/agda#8088) [1] > >> This needs investigation. > > well then investigate it. These simplified and reduced source for GCDTest-Agda...
Yes. It is not compiled with profiling, there is GHC error.
I could find the ticket if you ask. But probably its pointer in not needed, because this error in GHC is fixed in ghc-9.12.2.20250919 and probably in the further versions...