Skip to content

Commit d8f1e47

Browse files
committed
narrow imports
1 parent df74251 commit d8f1e47

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Relation/Nullary/Reflects.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ open import Data.Bool.Base
1414
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
1515
open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
1616
open import Level using (Level)
17-
open import Function.Base using (_$_; _∘_; const; id; flip)
17+
open import Function.Base using (_$_; _∘_; const; id)
1818
open import Relation.Nullary.Negation.Core using (¬_; weak-contradiction; _¬-⊎_)
1919
open import Relation.Nullary.Recomputable using (Recomputable)
2020

0 commit comments

Comments
 (0)