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]
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!