From 29157501d4f6cc2e9d98bfd36d0c37601aa3661f Mon Sep 17 00:00:00 2001 From: wadler Date: Fri, 17 Apr 2020 12:14:55 -0300 Subject: [PATCH] added proj_2 to imports in Qualifiers --- src/plfa/part1/Quantifiers.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part1/Quantifiers.lagda.md b/src/plfa/part1/Quantifiers.lagda.md index 6de734ff..dd160e0c 100644 --- a/src/plfa/part1/Quantifiers.lagda.md +++ b/src/plfa/part1/Quantifiers.lagda.md @@ -19,7 +19,7 @@ import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl) open import Data.Nat using (ℕ; zero; suc; _+_; _*_) open import Relation.Nullary using (¬_) -open import Data.Product using (_×_; proj₁) renaming (_,_ to ⟨_,_⟩) +open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩) open import Data.Sum using (_⊎_) open import plfa.part1.Isomorphism using (_≃_; extensionality) ```