chore: make Dec-→ incoherent

It overlaps with `Dec-Fin-∀`.
the1lab · Jan 6, 2025 · c35ef2a · c35ef2a
1 parent d1d6951
commit c35ef2a
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/Data/Dec/Base.lagda.md b/src/Data/Dec/Base.lagda.md
@@ -153,6 +153,7 @@ instance
   Dec-→ {Q = _} ⦃ yes p ⦄ ⦃ yes q ⦄ = yes λ _ → q
   Dec-→ {Q = _} ⦃ yes p ⦄ ⦃ no ¬q ⦄ = no λ pq → ¬q (pq p)
   Dec-→ {Q = _} ⦃ no ¬p ⦄ ⦃ q ⦄ = yes λ p → absurd (¬p p)
+  {-# INCOHERENT Dec-→ #-}
 
   Dec-⊤ : Dec ⊤
   Dec-⊤ = yes tt