Comment by markusde

I'm curious what you like about Agda functional programming? Many of the praises I hear about it have to do with it's dependent pattern matching, and I think Lean suffers a lot more in that regard. I'm curious though if you still find Agda friendlier for "normal" fp (and if so, how?)