From 2871611bec3b3267d52fe80b1545724be67b6331 Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Thu, 8 Feb 2018 14:31:35 -0400
Subject: [PATCH] updated Agda

---
 src/Equivalence.lagda | 5 ++---
 src/Lists.lagda       | 3 ---
 2 files changed, 2 insertions(+), 6 deletions(-)

diff --git a/src/Equivalence.lagda b/src/Equivalence.lagda
index 9dd88d46..f3e48235 100644
--- a/src/Equivalence.lagda
+++ b/src/Equivalence.lagda
@@ -281,11 +281,10 @@ that `even (n + m)` holds.
 
 Agda includes special notation to support just this
 kind of reasoning.  To enable this notation, we use
-pragmas to tell Agda which types and constructors
-correspond to equivalence and refl.
+pragmas to tell Agda which type
+corresponds to equivalence.
 \begin{code}
 {-# BUILTIN EQUALITY _≡_ #-}
-{-# BUILTIN REFL refl #-}
 \end{code}
 
 We can then prove the desired property as follows.
diff --git a/src/Lists.lagda b/src/Lists.lagda
index 047b2d0c..ff046a6e 100644
--- a/src/Lists.lagda
+++ b/src/Lists.lagda
@@ -14,7 +14,6 @@ import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; sym; trans; cong)
 open Eq.≡-Reasoning
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
-open import Data.Nat.Properties.Simple using (distribʳ-*-+; *-comm)
 \end{code}
 
 ## Lists
@@ -72,8 +71,6 @@ of `List A` by `List ℕ`, say.
 Including the lines
 \begin{code}
 {-# BUILTIN LIST List #-}
-{-# BUILTIN NIL  []   #-}
-{-# BUILTIN CONS _∷_  #-}
 \end{code}
 tells Agda that the type `List` corresponds to the Haskell type
 list, and the constructors `[]` and `_∷_` correspond to nil and