Skip to content

Commit ca36bfc

Browse files
ncfavierplt-amy
authored andcommitted
chore: make Dec-→ incoherent
It overlaps with `Dec-Fin-∀`.
1 parent d1d6951 commit ca36bfc

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

src/Data/Dec/Base.lagda.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -153,6 +153,7 @@ instance
153153
Dec-→ {Q = _} ⦃ yes p ⦄ ⦃ yes q ⦄ = yes λ _ → q
154154
Dec-→ {Q = _} ⦃ yes p ⦄ ⦃ no ¬q ⦄ = no λ pq → ¬q (pq p)
155155
Dec-→ {Q = _} ⦃ no ¬p ⦄ ⦃ q ⦄ = yes λ p → absurd (¬p p)
156+
{-# INCOHERENT Dec-→ #-}
156157
157158
Dec-⊤ : Dec ⊤
158159
Dec-⊤ = yes tt

0 commit comments

Comments
 (0)