Skip to content

Commit ade4110

Browse files
committed
[ minor ] remove implicit argument application from transitive
1 parent 5110d22 commit ade4110

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Relation/Binary/Construct/Interior/Symmetric.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,7 @@ trans′ : Trans R S T → Trans S R T →
5151
trans′ trans-rs trans-sr (r , r′) (s , s′) = trans-rs r s , trans-sr s′ r′
5252

5353
transitive : Transitive R Transitive (SymInterior R)
54-
transitive {R = R} tr = trans′ {R = R} tr tr
54+
transitive tr = trans′ tr tr
5555

5656
-- The symmetric interior of a strict relation is empty.
5757
Empty-SymInterior : Asymmetric R Empty (SymInterior R)

0 commit comments

Comments
 (0)