[murbard2]

It's great to have an example, but could you add inline comments for those of us who aren't familiar with Agda's syntax?

[Retra]

It's basically Haskell with unicode identifiers and mixed-fixity. (I.e., _::_ is an infix function of two arguments, and the _'s represent "holes" for the arguments.)