From 5e3a40651591318dabee3b104e2367b5bfe64002 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 16 Aug 2023 16:47:00 +0100 Subject: [PATCH] removed redundant `import`s from `Data.Bool.Base` --- src/Data/List/NonEmpty/Base.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Data/List/NonEmpty/Base.agda b/src/Data/List/NonEmpty/Base.agda index 320cacd4b6..82f16c270a 100644 --- a/src/Data/List/NonEmpty/Base.agda +++ b/src/Data/List/NonEmpty/Base.agda @@ -9,8 +9,7 @@ module Data.List.NonEmpty.Base where open import Level using (Level) -open import Data.Bool.Base using (Bool; false; true; not; T) -open import Data.Bool.Properties using (T?) +open import Data.Bool.Base using (Bool; false; true) open import Data.List.Base as List using (List; []; _∷_) open import Data.Maybe.Base using (Maybe ; nothing; just) open import Data.Nat.Base as ℕ