Nils Anders Danielsson

OK, thanks.

I looked at the example that you linked to. One slow part involved checking that `GroupHom (coHomGr 1 (A ⋁ B)) (×coHomGr 1 (typ A) (typ B))` was convertible to...

I tried to define a copattern synonym today. It took a while before I realised that Agda does not support them. I got error messages of the following kind: ```...

#2735 is not completely fixed, because numbered links are used for names coming from opened parametrised modules.

I also made an attempt to implement the feature request from issue #3198.

> #2735 is not completely fixed, because numbered links are used for names coming from opened parametrised modules. I moved that part of issue #2735 to another issue (#5974). >...

> The information that I use is whether a given name is exported (perhaps qualified) from the top-level module in which it is declared. Is there an easy (and efficient)...

Should `--cumulativity` be made incompatible with `--safe`?

Perhaps we shouldn't have both `--exact-split` and the corresponding warning. Can one enable `-Werror` for a subset of warnings, and still have other warnings enabled?

I have another example that checks without problems without `-Werror`, but fails with `-Werror`. I'll try to construct a small test case later.