Skip to content

Commit 8ad7b41

Browse files
committed
fix: imports
1 parent 84c9420 commit 8ad7b41

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Data/Fin/Permutation.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ open import Function.Base using (_∘_)
2626
open import Level using (0ℓ)
2727
open import Relation.Binary.Core using (Rel)
2828
open import Relation.Nullary using (does; ¬_; yes; no)
29-
open import Relation.Nullary.Decidable using (dec-yes; dec-no)
29+
open import Relation.Nullary.Decidable using (dec-no)
3030
open import Relation.Nullary.Negation using (contradiction)
3131
open import Relation.Binary.PropositionalEquality.Core
3232
using (_≡_; _≢_; refl; sym; trans; subst; cong; cong₂)

0 commit comments

Comments
 (0)