Skip to content

Commit e37fe2a

Browse files
committed
refactoring; rename qualified import
1 parent 96175ed commit e37fe2a

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/Relation/Unary.agda

+2-2
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ open import Data.Sum.Base using (_⊎_; [_,_])
1515
open import Function.Base using (_∘_; _|>_)
1616
open import Level using (Level; _⊔_; 0ℓ; suc; Lift)
1717
open import Relation.Nullary.Decidable.Core using (Dec; True)
18-
open import Relation.Nullary.Negation.Core as Negation using (¬_)
18+
open import Relation.Nullary.Negation.Core as Nullary using (¬_)
1919
open import Relation.Binary.PropositionalEquality.Core using (_≡_)
2020

2121
private
@@ -165,7 +165,7 @@ syntax IUniversal P = ∀[ P ]
165165
-- Stability - instances of P are stable wrt double negation
166166

167167
Stable : Pred A ℓ Set _
168-
Stable P = x Negation.Stable (P x)
168+
Stable P = x Nullary.Stable (P x)
169169

170170
-- Decidability - it is possible to determine if an arbitrary element
171171
-- satisfies P.

0 commit comments

Comments
 (0)