Skip to content

Commit ef5056e

Browse files
authored
[Refractor] contradiction over ⊥-elim inData/List/Fresh/Membership/Setoid/Properties (#2668)
* [Refractor] contradiction over ⊥-elim in * remove bot elim from importation * add bot elim
1 parent 427d373 commit ef5056e

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Data/List/Membership/Setoid/Properties.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ open import Relation.Binary.Definitions as Binary hiding (Decidable)
3232
open import Relation.Binary.Bundles using (Setoid)
3333
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
3434
open import Relation.Nullary.Decidable using (does; _because_; yes; no)
35-
open import Relation.Nullary.Negation using (¬_; contradiction)
35+
open import Relation.Nullary.Negation.Core using (¬_; contradiction)
3636
open import Relation.Nullary.Reflects using (invert)
3737
open import Relation.Unary as Unary using (Decidable; Pred)
3838

0 commit comments

Comments
 (0)