From 24e0361dbb4fc45048a02862aef40d691265dfed Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Tue, 15 Oct 2024 09:12:29 +0100 Subject: [PATCH] fix imports for Negation (#1049) --- src/plfa/part1/Negation.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/plfa/part1/Negation.lagda.md b/src/plfa/part1/Negation.lagda.md index 638808b46..6a093a5c8 100644 --- a/src/plfa/part1/Negation.lagda.md +++ b/src/plfa/part1/Negation.lagda.md @@ -15,9 +15,9 @@ and classical logic. ```agda open import Relation.Binary.PropositionalEquality using (_≡_; refl) open import Data.Nat using (ℕ; zero; suc) -open import Data.Empty using (⊥) +open import Data.Empty using (⊥; ⊥-elim) open import Data.Sum using (_⊎_; inj₁; inj₂) -open import Data.Product using (_×_) +open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩) open import Relation.Nullary.Negation using (contradiction) open import plfa.part1.Isomorphism using (_≃_; extensionality) ```