Nils Anders Danielsson

> For instance, several of my proofs take a hard dependence on the definition of `_++_` for lists. If the library were changed to pattern match on the right argument...

> [@nad](https://github.com/nad) implemented option `--no-syntactic-equality` (see https://agda.readthedocs.io/en/v2.7.0.1/tools/command-line-options.html#cmdoption-no-syntactic-equality) to turn off a short-cut in equality checking. No, it was @jespercockx (50c9cc29c4e944da3d9e43c964f39ecb46490850).

I could make your code type-check quickly by making `functor=` opaque. (After replacing the pattern-matching lambdas in its type with regular lambdas.)

Nowadays I make most definitions opaque, and I recommend that you try the same strategy. If you do not want to go that far, then you can at least follow...

> So there must be some kind of non-trivial difference between certain definitions / proofs that mean that some should be unfolded and some should be. It is in general...

> Thanks! (IIUC none of those are compatible with --safe, so they're also not options for me, but I appreciate the tips.) Instead of postulating `a : A` you can...

For a list of binary trees I might want to split `ts` into `t ∷ ts`, but for the node constructor I might instead want to split `t` into `node...

At the moment `x` is used, but not names for recursive arguments.

> Maybe we could use reflection to let users write their own name generators. So the user would write a function `namesForType : Term -> TC (Stream String)` (or something...

I don't think `unquoteDecl` is nice syntax for this kind of thing, its name suggests that you actually unquote a declaration, even if (going by the documentation) this might not...