We upgraded to Agda 2.6.1 and version 1.3 of the standard library. If you want to continue working with the latest version of the book, you’ll have to update your versions locally. Please follow the instructions in Getting Started to reinstall Agda and the standard library.

Changes to the termination checker

Agda 2.6.1 made several changes to the termination checker. As a result of these changes, Agda is no longer able to see that our evaluation functions, e.g., in Properties, are terminating. In response, we changed the definition of Gas to be a record type, rather than a data type:

- data Gas : Set where
-   gas : ℕ → Gas
+ record Gas : Set where
+   constructor gas
+   field
+     amount : ℕ

The reason this works is that η-equality holds by definition for records. Agda uses this to see that unwrapping and rewrapping numbers as Gas is the identity, and hence the amount of gas is decreasing if that number is decreasing.

Changes to equational reasoning

The function _≡⟨_⟩_, part of the equational reasoning syntax, was renamed to step-≡, for various reasons. The new function has the same semantics, but flips the order of the arguments. This does not mean you have to change your equational reasoning proofs, as the module also defines a syntax macro, which recovers the original argument order:

infixr -2 step-≡

step-≡ : ∀ x {y z : A} → y ≡ z → x ≡ y → x ≡ z
step-≡ y≡z x≡y = trans x≡y y≡z

syntax step-≡ x y≡z x≡y = x ≡⟨ x≡y ⟩ y≡z

Syntax macros aren’t quite definitions in Agda, so you cannot import them by “name”. Instead, they’re imported together with the function for which they’re defined, i.e., as step-≡:

- open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
+ open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)

If you’d like more details, there’s a lot of discussion of why this change was made in the CHANGELOG. For PLFA, we make a note of the incongruence in the chapter on Equality, but leave our definitions of equational reasoning unchanged.

Deprecation of Data.List.{All,Any}

The modules Data.List.{All,Any} were deprecated in v1.0, and were moved to Data.List.Relation.Unary.{All,Any}:

- import Data.List.All using (All; []; _∷_)
- import Data.List.Any using (Any; here; there)
+ import Data.List.Relation.Unary.All using (All; []; _∷_)
+ import Data.List.Relation.Unary.Any using (Any; here; there)