Agda 2.4.2 has been released! It comes with an experimental implementation of "type" classes (see "instance search" below). Download with cabal install Agda-2.4.2 (might need cabal update first) or go to http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Download. Highlights: - Recursive instance search. Instance arguments are much faster than before and now work like a proper class system. - Major improvements to reflection - Quoting and unquoting of declarations and pattern matching lambdas. - New syntax to simplify using reflection: tactic f is sugar for quoteGoal g in unquote (f g) More details here: https://github.com/agda/agda/blob/2.4.2/doc/release-notes/2-4-2.txt -- Andreas Abel <>< Du bist der geliebte Mensch. Department of Computer Science and Engineering Chalmers and Gothenburg University, Sweden andreas.abel@gu.se http://www2.tcs.ifi.lmu.de/~abel/ -- Andreas Abel <>< Du bist der geliebte Mensch. Department of Computer Science and Engineering Chalmers and Gothenburg University, Sweden andreas.abel@gu.se http://www2.tcs.ifi.lmu.de/~abel/