Orestis Melkonian

I think it's important to contrast two different approaches to declaring superclasses and choose one for the standard library after careful consideration. Here's an example of the `Eq` typeclass and...

I have personally come to love this ugly bugger, so I propose we keep it as is (but remove `map-with-∈` ofc).

> Can you explain the "fall back when the freeze plan is different" bit? does it mean that if the freeze file is different from the cache, it will not...

> If you're looking at this and saying to yourself "wow, that looks particularly verbose and error-prone", that's because it is. Now that github exposes the cache API in nodejs,...

> I rebased @WhatisRT's change on the [current](https://github.com/agda/agda/commit/a37b3b4717f202716a2f0487c824b771506b3101) master branch and solved conflicts. But I don't know how to (force) push my change to his branch. May @WhatisRT can have...

> @omelkonian : You are a power user of instance search. Would you be affected by changes proposed here? E.g., if instances could not come into scope from visible arguments......

> Does it work if you comment out the `instance _ : Dec ⊤`? The error message to me looks like a case of overlap (Agda refuses to decide between...

OK, that makes some sense, it just didn't occur to me that the order of fields matters. However, this still doesn't explain why the same thing using `record` is not...

Another resource: how [GHC](https://hackage.haskell.org/package/ghc) does plugins without using the aforementioned `plugins` package: - https://hackage.haskell.org/package/ghc-9.8.1/docs/GHC-Driver-Plugins.html - https://hackage.haskell.org/package/ghc-9.8.1/docs/GHC-Driver-Plugins-External.html

> I'm a bit confused by what's the purpose of this PR. We already have the `C-c C-x C-c` for compiling the current file with a given backend, how would...