Skip to content

Commit 1e3a519

Browse files
authored
fix Connex comment (#2204)
Connex allows both relations to hold, so the old comment was wrong.
1 parent 1532a50 commit 1e3a519

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Relation/Binary/Definitions.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -99,7 +99,7 @@ Asymmetric _<_ = ∀ {x y} → x < y → ¬ (y < x)
9999
Dense : Rel A ℓ Set _
100100
Dense _<_ = {x y} x < y ∃[ z ] x < z × z < y
101101

102-
-- Generalised connex - exactly one of the two relations holds.
102+
-- Generalised connex - at least one of the two relations holds.
103103

104104
Connex : REL A B ℓ₁ REL B A ℓ₂ Set _
105105
Connex P Q = x y P x y ⊎ Q y x

0 commit comments

Comments
 (0)