Skip to content

Commit b69dc60

Browse files
Fix bug in multi-setoid reasoning introduced after v1.2
1 parent 1e48171 commit b69dc60

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Relation/Binary/Reasoning/MultiSetoid.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -76,6 +76,6 @@ module _ {c ℓ} {S : Setoid c ℓ} where
7676
_∎ _ = relTo refl
7777

7878
syntax step-≈ x y∼z x≈y = x ≈⟨ x≈y ⟩ y∼z
79-
syntax step-≈˘ x y∼z y≈x = x ≈⟨˘ y≈x ⟩ y∼z
79+
syntax step-≈˘ x y∼z y≈x = x ≈˘⟨ y≈x ⟩ y∼z
8080
syntax step-≡ x y≡z x≡y = x ≡⟨ x≡y ⟩ y≡z
8181
syntax step-≡˘ x y≡z y≡x = x ≡˘⟨ y≡x ⟩ y≡z

0 commit comments

Comments
 (0)