[Agda] Agda 2.4.0.2 released

[Andreas Abel]

The next maintenance release of Agda 2.4.0 is out!  It has mainly 
bug-fixes, plus a few small new features.

Get it with cabal from hackage or download from the Agda wiki!

   http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Download

   https://hackage.haskell.org/package/Agda

Have fun,
Andreas

Important changes since 2.4.0.1:

* The Agda input mode now supports alphabetical super and subscripts,
   in addition to the numerical ones that were already present.
   [Issue 1240]

* New feature: Interactively split result.

   Make case (C-c C-c) with no variables given tries to split on the
   result to introduce projection patterns.  The hole needs to be of
   record type, of course.

     test : {A B : Set} (a : A) (b : B) → A × B
     test a b = ?

   Result-splitting ? will produce the new clauses:

     proj₁ (test a b) = ?
     proj₂ (test a b) = ?

   If hole is of function type ending in a record type, the necessary
   pattern variables will be introduced before the split.  Thus, the
   same result can be obtained by starting from:

     test : {A B : Set} (a : A) (b : B) → A × B
     test = ?

* The so far undocumented ETA pragma now throws an error if applied to
   definitions that are not records.

   ETA can be used to force eta-equality at recursive record types,
   for which eta is not enabled automatically by Agda.
   Here is such an example:

     mutual
       data Colist (A : Set) : Set where
         [] : Colist A
         _∷_ : A → ∞Colist A → Colist A

       record ∞Colist (A : Set) : Set where
         coinductive
         constructor delay
         field       force : Colist A

     open ∞Colist

     {-# ETA ∞Colist #-}

     test : {A : Set} (x : ∞Colist A) → x ≡ delay (force x)
     test x = refl

   Note:  Unsafe use of ETA can make Agda loop, e.g. by triggering
   infinite eta expansion!

* Bugs fixed (see https://code.google.com/p/agda/issues):
   1203
   1205
   1209
   1213
   1214
   1216
   1225
   1226
   1231
   1233
   1239
   1241
   1243

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/