2.4.0.2.md

Release notes for Agda 2 version 2.4.0.2
========================================

* The Agda input mode now supports alphabetical super and subscripts,
  in addition to the numerical ones that were already present.
  [Issue [#1240](https://github.com/agda/agda/issues/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.

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

  Result-splitting `?` will produce the new clauses:

  ```agda
  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:

  ```agda
  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:

  ```agda
  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 [bug tracker](https://github.com/agda/agda/issues)):

  [#1203](https://github.com/agda/agda/issues/1203)

  [#1205](https://github.com/agda/agda/issues/1205)

  [#1209](https://github.com/agda/agda/issues/1209)

  [#1213](https://github.com/agda/agda/issues/1213)

  [#1214](https://github.com/agda/agda/issues/1214)

  [#1216](https://github.com/agda/agda/issues/1216)

  [#1225](https://github.com/agda/agda/issues/1225)

  [#1226](https://github.com/agda/agda/issues/1226)

  [#1231](https://github.com/agda/agda/issues/1231)

  [#1233](https://github.com/agda/agda/issues/1233)

  [#1239](https://github.com/agda/agda/issues/1239)

  [#1241](https://github.com/agda/agda/issues/1241)

  [#1243](https://github.com/agda/agda/issues/1243)