Skip to content

Commit e0d2d5e

Browse files
jamesmckinnaMatthewDaggitt
authored andcommitted
Removed redundant imports from Data.Bool.Base (#2062)
1 parent ccdb4b3 commit e0d2d5e

File tree

1 file changed

+1
-2
lines changed

1 file changed

+1
-2
lines changed

src/Data/List/NonEmpty/Base.agda

+1-2
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,7 @@
99
module Data.List.NonEmpty.Base where
1010

1111
open import Level using (Level)
12-
open import Data.Bool.Base using (Bool; false; true; not; T)
13-
open import Data.Bool.Properties using (T?)
12+
open import Data.Bool.Base using (Bool; false; true)
1413
open import Data.List.Base as List using (List; []; _∷_)
1514
open import Data.Maybe.Base using (Maybe ; nothing; just)
1615
open import Data.Nat.Base as ℕ

0 commit comments

Comments
 (0)