fix imports for Negation (#1049)

plfa · Oct 15, 2024 · 24e0361 · 24e0361
1 parent 7aadc35
commit 24e0361
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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)
 ```