valis

or by broken caches in IDE.

Yes, it happens a lot. We have a bunch of issues that are intendent to fix this.

Maybe

Can you reproduce it?

Fixed the code

This is a generalization of #187.

In the last two examples, that's impossible because after '\extends' it expects a name and not an arbitrary expression. And what's the point of putting a goal there anyway?

This is a special case of #214.

Can't you just write ``` \func transport-code-loop : transport code (path loop) = isuc => transport-ap-assoc code (path loop) ``` ?

Even `\func transport-code-loop : transport code (path loop) = isuc => idp` works.