From 6428b87def95c2a1e40d9d4620052f758d18f7ae Mon Sep 17 00:00:00 2001 From: wadler Date: Sat, 18 Apr 2020 12:20:03 -0300 Subject: [PATCH] added import to 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 dd160e0c..7d4ccfc0 100644 --- a/src/plfa/part1/Quantifiers.lagda.md +++ b/src/plfa/part1/Quantifiers.lagda.md @@ -20,7 +20,7 @@ open Eq using (_≡_; refl) open import Data.Nat using (ℕ; zero; suc; _+_; _*_) open import Relation.Nullary using (¬_) open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩) -open import Data.Sum using (_⊎_) +open import Data.Sum using (_⊎_; inj₁; inj₂) open import plfa.part1.Isomorphism using (_≃_; extensionality) ```