agda/doc/release-notes/2.4.2.5.md

Release notes for Agda version 2.4.2.5

Installation and infrastructure

• Added support for GHC 7.10.3.

• Added cpphs Cabal flag

Turn on/off this flag to choose cpphs/cpp as the C preprocessor.

This flag is turn on by default.

(This flag was added in Agda 2.4.2.1 but it was not documented)

Pragmas and options

• Termination pragmas are no longer allowed inside where clauses [Issue #1137].

Type checking

• with-abstraction is more aggressive, abstracts also in types of variables that are used in the with-expressions, unless they are also used in the types of the with-expressions. [Issue #1692]

Example:

  test : (f : (x : A) → a ≡ x) (b : A) → b ≡ a
  test f b with a | f b
  test f b | .b | refl = f b

Previously, with would not abstract in types of variables that appear in the with-expressions, in this case, both f and b, leaving their types unchanged. Now, it tries to abstract in f, as only b appears in the types of the with-expressions which are A (of a) and a ≡ b (of f b). As a result, the type of f changes to (x : A) → b ≡ x and the type of the goal to b ≡ b (as previously).

This also affects rewrite, which is implemented in terms of with.

  test : (f : (x : A) → a ≡ x) (b : A) → b ≡ a
  test f b rewrite f b = f b

As the new with is not fully backwards-compatible, some parts of your Agda developments using with or rewrite might need maintenance.

Fixed issues

See bug tracker

#1407

#1518

#1670

#1677

#1698

#1701

#1710

#1718