[Agda] signature for `with' branch

[Nils Anders Danielsson]

On 2017-02-27 13:43, Sergei Meshveliani wrote:
> Sometimes I manage to set a signature for `aux' in the branch.
> Then, this helps a lot, because from `aux', the `with' sequence can be
> started by new, and the problem is split to parts.

If this helps a lot, then I suggest that you do not use with at all. The
with expressions are translated into regular Agda code, that you could
have written yourself, with some exceptions, one of which is that with
applications are not parsed (but they are not needed if you do not use
with).

-- 
/NAD