[Agda] The joys and sorrows of abstraction

[Wolfram Kahl]

On Tue, May 15, 2018 at 07:27:37PM -0300, Philip Wadler wrote:
> The definitions of make, prefix, and suffix are quite involved, so in order
> to prevent them expanding to unreadable length in proofs I have made them
> and the corresponding lemmas abstract.

You could try to make them module parameters instead,
and later supply the implementation where needed.


Wolfram