[Agda] The joys and sorrows of abstraction

[Andrew Pitts]

On 16 May 2018 at 22:24, Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:
> One good thing about Agda is that it can be very readable, if you write
> well.

For me this aspect of Agda is very important and why I have ended up
using it. Access to dependent pattern matching is a crucial part of
what makes it so nice. And even if Agda does not do it that way for
historical reasons, we do apparently have a good account of
elaborating such patterms to elimation combinators. (From what I
understand, this is used by Lean to translate code with patterns back
into its core type theory.)

(The co-patterns of Andreas et al are also very good for making
readable definitions; I’m not so sure if they have firm foundations —
pardon my ignorance.)

Andy