Skip to content

Commit 0095ffc

Browse files
jmougeotjamesmckinna
authored andcommitted
[Refractor] contradiction over ⊥-elim inData/List/Fresh/Membership/Setoid/Properties (agda#2668)
* [Refractor] contradiction over ⊥-elim in * remove bot elim from importation * add bot elim
1 parent 8318834 commit 0095ffc

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)