[Agda] Simple Agda Libraries

Andres Loeh andres at cs.uu.nl
Thu Jan 15 08:35:10 CET 2009


FWIW, I share Shin-Cheng's impression of the standard library.
Initially, I was quite sceptic and found it difficult to use, but
after being forced to use it regularly while preparing for a course
on Agda I taught, I started to actually like it.

The use of Unicode with Emacs is simple enough. The only reason I
sometimes find it annoying is that it's not as easy to grep for unicode
symbols from the shell as it is for normal identifiers.

I really like the powerful mixfix operators and often find them easier
to read (because easier to remember / closer to the notation I'm
familiar with from papers) than just infix operators.

Cheers,
  Andres

-- 

Andres Loeh, Universiteit Utrecht

mailto:andres at cs.uu.nl     mailto:mail at andres-loeh.de
http://www.andres-loeh.de


More information about the Agda mailing list