Skip to content

Commit 59306b9

Browse files
authored
fix: redundant import (#2707)
1 parent 6db08b3 commit 59306b9

File tree

1 file changed

+0
-1
lines changed

1 file changed

+0
-1
lines changed

src/Data/Fin/Base.agda

-1
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,6 @@
1111

1212
module Data.Fin.Base where
1313

14-
open import Data.Bool.Base using (Bool; T)
1514
open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
1615
open import Data.Product.Base as Product using (_×_; _,_; proj₁; proj₂)
1716
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)

0 commit comments

Comments
 (0)