Wolfram Kahl

https://github.com/agda/agda-ghc-names --- but I haven't updated it in a long time.

I occasionally use names like `foldrNE`.

Only now I got around to try this out --- I applied it to the current development version, and it works wonders! It is not slower on any of the...

From extensive experience using this patch: Losing solutions only raises the problem that some metas are resolved with this patch that wouldn't be resolved without it. Practically that means that...

@HuStmpHrrr , ncatlab is a somewhat surprising source for relation-algebraic terminology. A more common starting point, which I am also using in [RATH-Agda](http://RelMiCS.McMaster.ca/RATHAgda/), is the following textbook: ```bibtex @Book{Schmidt-Stroehlein-1993, author...

@MatthewDaggitt, you could choose to not change that field name, arguing that some people use the name “total” for this property in the order context. (However, I still much prefer...

Thank you very much for that link --- that is very useful! This appears to explain at least some of the trouble I am having with refactoring fragments of `lincat`...

My first point was that as user, I don't expect to see internal errors, but assume that the developers would like to be informed when I do see one, since...

Yes. :wink: If you want them inside, you can also define `↓_ = ≡-sym` with appropriate low precedence. Having the arrows after the closing hint bracket looks more acceptable to...

Possibly as an alternative, it would be helpful if `haste-boot` would respect ``` user-install: False install-dirs global prefix: /usr/local/packages/MyPrefix ``` from my `.cabal/config` (which is referred to from `haste-cabal`, but...