From 0615638d66e8615407310063c4e3f130392677b3 Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Sun, 19 Jul 2020 19:43:20 +0100
Subject: [PATCH] Upgrade to Agda v2.6.1. (#492)

---
 README.md                              | 23 ++++++++++++-----------
 courses/tspl/2019/Assignment1.lagda.md |  6 +++---
 courses/tspl/2019/Assignment2.lagda.md |  3 +--
 courses/tspl/2019/Assignment3.lagda.md |  3 +--
 courses/tspl/2019/Assignment4.lagda.md |  6 ++++--
 courses/tspl/2019/Exam.lagda.md        |  6 ++++--
 src/plfa/part1/Equality.lagda.md       | 14 +++++++++-----
 src/plfa/part1/Induction.lagda.md      |  4 ++--
 src/plfa/part1/Lists.lagda.md          |  4 ++--
 src/plfa/part2/DeBruijn.lagda.md       |  7 ++++---
 src/plfa/part2/More.lagda.md           |  6 ++++--
 src/plfa/part2/Properties.lagda.md     | 11 ++++++-----
 src/plfa/part2/Substitution.lagda.md   |  2 +-
 src/plfa/part2/Untyped.lagda.md        |  8 +++++---
 src/plfa/part3/Denotational.lagda.md   |  9 +++------
 15 files changed, 61 insertions(+), 51 deletions(-)

diff --git a/README.md b/README.md
index 54c13972..a899dff0 100644
--- a/README.md
+++ b/README.md
@@ -6,6 +6,7 @@ permalink: /GettingStarted/
 
 <!-- Links -->
 
+[epub]: https://plfa.github.io/out/epub/plfa.epub
 [plfa]: http://plfa.inf.ed.ac.uk
 [plfa-dev]: https://github.com/plfa/plfa.github.io/archive/dev.zip
 [plfa-status]: https://travis-ci.org/plfa/plfa.github.io.svg?branch=dev
@@ -14,14 +15,14 @@ permalink: /GettingStarted/
 [plfa-latest]: https://github.com/plfa/plfa.github.io/releases/latest
 [plfa-master]: https://github.com/plfa/plfa.github.io/archive/master.zip
 
-[agda]: https://github.com/agda/agda/releases/tag/v2.6.0.1
-[agda-version]: https://img.shields.io/badge/agda-v2.6.0.1-blue.svg
-[agda-docs-emacs-mode]: https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.html
-[agda-docs-emacs-notation]: https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.html#notation-for-key-combinations
-[agda-docs-package-system]: https://agda.readthedocs.io/en/v2.6.0.1/tools/package-system.html#example-using-the-standard-library
+[agda]: https://github.com/agda/agda/releases/tag/v2.6.1
+[agda-version]: https://img.shields.io/badge/agda-v2.6.1-blue.svg
+[agda-docs-emacs-mode]: https://agda.readthedocs.io/en/v2.6.1/tools/emacs-mode.html
+[agda-docs-emacs-notation]: https://agda.readthedocs.io/en/v2.6.1/tools/emacs-mode.html#notation-for-key-combinations
+[agda-docs-package-system]: https://agda.readthedocs.io/en/v2.6.1/tools/package-system.html#example-using-the-standard-library
 
-[agda-stdlib-version]: https://img.shields.io/badge/agda--stdlib-v1.1-blue.svg
-[agda-stdlib]: https://github.com/agda/agda-stdlib/releases/tag/v1.1
+[agda-stdlib-version]: https://img.shields.io/badge/agda--stdlib-v1.3-blue.svg
+[agda-stdlib]: https://github.com/agda/agda-stdlib/releases/tag/v1.3
 
 [haskell-stack]:  https://docs.haskellstack.org/en/stable/README/
 [haskell-ghc]: https://www.haskell.org/ghc/
@@ -64,11 +65,11 @@ The easiest way to install any specific version of Agda is using [Stack][haskell
 ```bash
 git clone https://github.com/agda/agda.git
 cd agda
-git checkout v2.6.0.1
+git checkout v2.6.1
 ```
 To install Agda, run Stack from the Agda source directory:
 ```bash
-stack install --stack-yaml stack-8.6.5.yaml
+stack install --stack-yaml stack-8.8.3.yaml
 ```
 If you want Stack to use you system installation of GHC, you can pass the `--system-ghc` flag and select the appropriate `stack-*.yaml` file. For instance, if you have GHC 8.2.2 installed, run:
 ```bash
@@ -81,7 +82,7 @@ You can get the required version of the Agda standard library from GitHub, eithe
 ```bash
 git clone https://github.com/agda/agda-stdlib.git
 cd agda-stdlib
-git checkout v1.1
+git checkout v1.3
 ```
 You can get the latest version of Programming Language Foundations in Agda from GitHub, either by cloning the repository, or by downloading [the zip archive][plfa-dev]:
 ```bash
@@ -227,7 +228,7 @@ bundle exec jekyll serve
 
 ### Building the EPUB
 
-The EPUB version of the book is built using Pandoc. Here's how to build the EPUB:
+The [EPUB version][epub] of the book is built using Pandoc. Here's how to build the EPUB:
 
 1. Install a recent version of Pandoc, [available here][pandoc].
    We recommend their official installer (on the linked page),
diff --git a/courses/tspl/2019/Assignment1.lagda.md b/courses/tspl/2019/Assignment1.lagda.md
index cbc579b9..d5c2f94d 100644
--- a/courses/tspl/2019/Assignment1.lagda.md
+++ b/courses/tspl/2019/Assignment1.lagda.md
@@ -47,7 +47,7 @@ yourself, or your group in the case of group practicals).
 ```
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; cong; sym)
-open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
+open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; z≤n; s≤s)
 open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm;
   ≤-refl; ≤-trans; ≤-antisym; ≤-total; +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
@@ -142,7 +142,7 @@ Give an example of an operator that has an identity and is
 associative but is not commutative.
 
 
-#### Exercise `finite-+-assoc` (stretch) {#finite-plus-assoc}
+#### Exercise `finite-|-assoc` (stretch) {#finite-plus-assoc}
 
 Write out what is known about associativity of addition on each of the first four
 days using a finite story of creation, as
@@ -196,7 +196,7 @@ Show
 
 for all naturals `n`. Did your proof require induction?
 
-#### Exercise `∸-+-assoc` (practice) {#monus-plus-assoc}
+#### Exercise `∸-|-assoc` (practice) {#monus-plus-assoc}
 
 Show that monus associates with addition, that is,
 
diff --git a/courses/tspl/2019/Assignment2.lagda.md b/courses/tspl/2019/Assignment2.lagda.md
index 32820103..1aa8d8e0 100644
--- a/courses/tspl/2019/Assignment2.lagda.md
+++ b/courses/tspl/2019/Assignment2.lagda.md
@@ -45,7 +45,7 @@ yourself, or your group in the case of group practicals).
 ```
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; cong; sym)
-open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
+open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; z≤n; s≤s)
 open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm;
   ≤-refl; ≤-trans; ≤-antisym; ≤-total; +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
@@ -481,4 +481,3 @@ postulate
 ```
 -- Your code goes here
 ```
-
diff --git a/courses/tspl/2019/Assignment3.lagda.md b/courses/tspl/2019/Assignment3.lagda.md
index 5e00b72d..5c7c73e2 100644
--- a/courses/tspl/2019/Assignment3.lagda.md
+++ b/courses/tspl/2019/Assignment3.lagda.md
@@ -42,7 +42,7 @@ yourself, or your group in the case of group practicals).
 ```
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; cong; sym)
-open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
+open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
 open import Data.Bool.Base using (Bool; true; false; T; _∧_; _∨_; not)
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
 open import Data.Nat.Properties using
@@ -538,4 +538,3 @@ Provide proofs of the three postulates, `unstuck`, `preserves`, and `wttdgs` abo
 ```
 -- Your code goes here
 ```
-
diff --git a/courses/tspl/2019/Assignment4.lagda.md b/courses/tspl/2019/Assignment4.lagda.md
index 81a5b661..b2777e22 100644
--- a/courses/tspl/2019/Assignment4.lagda.md
+++ b/courses/tspl/2019/Assignment4.lagda.md
@@ -632,8 +632,10 @@ not fixed by the given arguments.
 ## Evaluation
 
 ```
-  data Gas : Set where
-    gas : ℕ → Gas
+  record Gas : Set where
+    constructor gas
+    field
+      amount : ℕ
 
   data Finished {Γ A} (N : Γ ⊢ A) : Set where
 
diff --git a/courses/tspl/2019/Exam.lagda.md b/courses/tspl/2019/Exam.lagda.md
index fa4fffb2..0624dee2 100644
--- a/courses/tspl/2019/Exam.lagda.md
+++ b/courses/tspl/2019/Exam.lagda.md
@@ -351,8 +351,10 @@ module Problem2 where
 ### Evaluation
 
 ```
-  data Gas : Set where
-    gas : ℕ → Gas
+  record Gas : Set where
+    constructor gas
+    field
+      amount : ℕ
 
   data Finished {Γ A} (N : Γ ⊢ A) : Set where
 
diff --git a/src/plfa/part1/Equality.lagda.md b/src/plfa/part1/Equality.lagda.md
index 860660de..3d3c6d2e 100644
--- a/src/plfa/part1/Equality.lagda.md
+++ b/src/plfa/part1/Equality.lagda.md
@@ -696,23 +696,27 @@ _∘_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C
 (g ∘ f) x  =  g (f x)
 ```
 
-Further information on levels can be found in the [Agda Wiki][wiki].
+Further information on levels can be found in the [Agda docs][docs].
 
-[wiki]: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.UniversePolymorphism
+[docs]: https://agda.readthedocs.io/en/v2.6.1/language/universe-levels.html
 
 
 ## Standard library
 
-Definitions similar to those in this chapter can be found in the
-standard library:
+Definitions similar to those in this chapter can be found in the standard
+library. The Agda standard library defines `_≡⟨_⟩_` as `step-≡`, [which reverses
+the order of the arguments][step-≡]. The standard library also defines a syntax
+macro, which is automatically imported whenever you import `step-≡`, which
+recovers the original argument order:
 ```
 -- import Relation.Binary.PropositionalEquality as Eq
 -- open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst)
--- open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
+-- open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
 ```
 Here the imports are shown as comments rather than code to avoid
 collisions, as mentioned in the introduction.
 
+[step-≡]: https://github.com/agda/agda-stdlib/blob/master/CHANGELOG/v1.3.md#changes-to-how-equational-reasoning-is-implemented
 
 ## Unicode
 
diff --git a/src/plfa/part1/Induction.lagda.md b/src/plfa/part1/Induction.lagda.md
index 99ecb0a8..055b7e4a 100644
--- a/src/plfa/part1/Induction.lagda.md
+++ b/src/plfa/part1/Induction.lagda.md
@@ -28,7 +28,7 @@ and some operations upon them.  We also import a couple of new operations,
 ```
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; cong; sym)
-open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
+open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)
 ```
 
@@ -656,7 +656,7 @@ time we are concerned with judgments asserting associativity:
 
 Now, we apply the rules to all the judgments we know about.  The base
 case tells us that `(zero + n) + p ≡ zero + (n + p)` for every natural
-`n` and `p`.  The inductive case tells us that if 
+`n` and `p`.  The inductive case tells us that if
 `(m + n) + p ≡ m + (n + p)` (on the day before today) then
 `(suc m + n) + p ≡ suc m + (n + p)` (today).
 We didn't know any judgments about associativity before today, so that
diff --git a/src/plfa/part1/Lists.lagda.md b/src/plfa/part1/Lists.lagda.md
index 18e816ed..ecd5f0f8 100644
--- a/src/plfa/part1/Lists.lagda.md
+++ b/src/plfa/part1/Lists.lagda.md
@@ -1106,8 +1106,8 @@ with their corresponding proofs.
 Definitions similar to those in this chapter can be found in the standard library:
 ```
 import Data.List using (List; _++_; length; reverse; map; foldr; downFrom)
-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)
 import Data.List.Membership.Propositional using (_∈_)
 import Data.List.Properties
   using (reverse-++-commute; map-compose; map-++-commute; foldr-++)
diff --git a/src/plfa/part2/DeBruijn.lagda.md b/src/plfa/part2/DeBruijn.lagda.md
index 29b75d44..309cae55 100644
--- a/src/plfa/part2/DeBruijn.lagda.md
+++ b/src/plfa/part2/DeBruijn.lagda.md
@@ -1043,8 +1043,10 @@ refer to preservation, since it is built-in to the definition of reduction.
 
 As previously, gas is specified by a natural number:
 ```
-data Gas : Set where
-  gas : ℕ → Gas
+record Gas : Set where
+  constructor gas
+  field
+    amount : ℕ
 ```
 When our evaluator returns a term `N`, it will either give evidence that
 `N` is a value or indicate that it ran out of gas:
@@ -1375,4 +1377,3 @@ This chapter uses the following unicode:
     ₆  U+2086  SUBSCRIPT SIX (\_6)
     ₇  U+2087  SUBSCRIPT SEVEN (\_7)
     ≠  U+2260  NOT EQUAL TO (\=n)
-
diff --git a/src/plfa/part2/More.lagda.md b/src/plfa/part2/More.lagda.md
index 632ab5c6..2f86c40d 100644
--- a/src/plfa/part2/More.lagda.md
+++ b/src/plfa/part2/More.lagda.md
@@ -1089,8 +1089,10 @@ progress (case× L M) with progress L
 ## Evaluation
 
 ```
-data Gas : Set where
-  gas : ℕ → Gas
+record Gas : Set where
+  constructor gas
+  field
+    amount : ℕ
 
 data Finished {Γ A} (N : Γ ⊢ A) : Set where
 
diff --git a/src/plfa/part2/Properties.lagda.md b/src/plfa/part2/Properties.lagda.md
index fa44242c..95023b21 100644
--- a/src/plfa/part2/Properties.lagda.md
+++ b/src/plfa/part2/Properties.lagda.md
@@ -382,7 +382,7 @@ which is well typed in the empty context is also well typed in an arbitrary
 context.  The _drop_ lemma asserts that a term which is well typed in a context
 where the same variable appears twice remains well typed if we drop the shadowed
 occurrence. The _swap_ lemma asserts that a term which is well typed in a
-context remains well typed if we swap two variables. 
+context remains well typed if we swap two variables.
 
 (Renaming is similar to the _context invariance_ lemma in _Software
 Foundations_, but it does not require the definition of
@@ -775,7 +775,7 @@ Where the construct introduces a bound variable we need to compare it
 with the substituted variable, applying the drop lemma if they are
 equal and the swap lemma if they are distinct.
 
-For Agda it makes a difference whether we write `x ≟ y` or 
+For Agda it makes a difference whether we write `x ≟ y` or
 `y ≟ x`. In an interactive proof, Agda will show which residual `with`
 clauses in the definition of `_[_:=_]` need to be simplified, and the
 `with` clauses in `subst` need to match these exactly. The guideline is
@@ -918,8 +918,10 @@ per unit of gas.
 By analogy, we will use the name _gas_ for the parameter which puts a
 bound on the number of reduction steps.  `Gas` is specified by a natural number:
 ```
-data Gas : Set where
-  gas : ℕ → Gas
+record Gas : Set where
+  constructor gas
+  field
+    amount : ℕ
 ```
 When our evaluator returns a term `N`, it will either give evidence that
 `N` is a value or indicate that it ran out of gas:
@@ -950,7 +952,6 @@ data Steps (L : Term) : Set where
 The evaluator takes gas and evidence that a term is well typed,
 and returns the corresponding steps:
 ```
-{-# TERMINATING #-}
 eval : ∀ {L A}
   → Gas
   → ∅ ⊢ L ⦂ A
diff --git a/src/plfa/part2/Substitution.lagda.md b/src/plfa/part2/Substitution.lagda.md
index 887c0c92..e5a25a12 100644
--- a/src/plfa/part2/Substitution.lagda.md
+++ b/src/plfa/part2/Substitution.lagda.md
@@ -48,7 +48,7 @@ system that _decides_ whether any two substitutions are equal.
 ```
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; sym; cong; cong₂; cong-app)
-open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
+open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
 open import Function using (_∘_)
 open import plfa.part2.Untyped
      using (Type; Context; _⊢_; ★; _∋_; ∅; _,_; Z; S_; `_; ƛ_; _·_;
diff --git a/src/plfa/part2/Untyped.lagda.md b/src/plfa/part2/Untyped.lagda.md
index 815d88d6..33a76ffb 100644
--- a/src/plfa/part2/Untyped.lagda.md
+++ b/src/plfa/part2/Untyped.lagda.md
@@ -467,7 +467,7 @@ _ =
   ∎
 ```
 After just two steps the top-level term is an abstraction,
-and `ζ` rules drive the rest of the normalisation. 
+and `ζ` rules drive the rest of the normalisation.
 
 
 ## Progress
@@ -547,8 +547,10 @@ As previously, progress immediately yields an evaluator.
 
 Gas is specified by a natural number:
 ```
-data Gas : Set where
-  gas : ℕ → Gas
+record Gas : Set where
+  constructor gas
+  field
+    amount : ℕ
 ```
 When our evaluator returns a term `N`, it will either give evidence that
 `N` is normal or indicate that it ran out of gas:
diff --git a/src/plfa/part3/Denotational.lagda.md b/src/plfa/part3/Denotational.lagda.md
index bb05e64f..3673205e 100644
--- a/src/plfa/part3/Denotational.lagda.md
+++ b/src/plfa/part3/Denotational.lagda.md
@@ -54,9 +54,6 @@ down a denotational semantics of the lambda calculus.
 
 ## Imports
 
-<!-- JGS: for equational reasoning
-open import Relation.Binary using (Setoid)
--->
 ```
 open import Agda.Primitive using (lzero; lsuc)
 open import Data.Empty using (⊥-elim)
@@ -589,7 +586,7 @@ denotation-setoid Γ = record
 -->
 <!--
   The following went inside the module ≃-Reasoning:
-  
+
   open import Relation.Binary.Reasoning.Setoid (denotation-setoid Γ)
     renaming (begin_ to start_; _≈⟨_⟩_ to _≃⟨_⟩_; _∎ to _☐) public
 -->
@@ -854,7 +851,7 @@ Dᶜ n (a[n] ∷ ls) = (D^suc n (a[n] ∷ ls)) ↦ (vec-last (a[n] ∷ ls)) ↦
   a successor function whose denotation is given by `D^suc`,
   and the start of the path (last of the vector).
   It returns the `n + 1` vertex in the path.
-  
+
         (D^suc (suc n) (a[n+1] ∷ a[n] ∷ ls)) ↦ (vec-last (a[n] ∷ ls)) ↦ a[n+1]
 
 The exercise is to prove that for any path `ls`, the meaning of the
@@ -870,7 +867,7 @@ apply-n zero = # 0
 apply-n (suc n) = # 1 · apply-n n
 
 church : (n : ℕ) → ∅ ⊢ ★
-church n = ƛ ƛ apply-n n 
+church n = ƛ ƛ apply-n n
 ```
 
 Prove the following theorem.