[Agda] The joys and sorrows of abstraction

[Martin Escardo]

On 16/05/18 23:08, Philip Wadler wrote:
> Martin,
> 
> Thank you for sketching your preferred subset. I must admit that 'with' 
> and implicits are two of my favourite features. In place of `with`, do 
> you simply use auxiliary functions? I thought that `with` and auxiliary 
> functions were meant to be equivalent?

I forgot to say that I also use Agda to communicate mathematics to 
fellow researchers that know type theory but not necessarily Agda.

Because the meaning of "with" is not obvious and self-explanatory, it 
doesn't work for this purpose.

One good thing about Agda is that it can be very readable, if you write 
well.

Martin