Skip to content

Commit fa3d902

Browse files
Removed empty where block flagged by v2.6.2
1 parent e89a0c1 commit fa3d902

File tree

1 file changed

+0
-1
lines changed

1 file changed

+0
-1
lines changed

src/Data/List/Relation/Unary/Any/Properties.agda

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -254,7 +254,6 @@ Any-×⁻ pq with Prod.map₂ (Prod.map₂ find) (find pq)
254254
≡⟨ P.cong₂ _,_ (lose∘find p) (lose∘find q) ⟩
255255

256256
(p , q) ∎
257-
where
258257

259258

260259
to∘from : pq Any-×⁺ {xs = xs} (Any-×⁻ pq) ≡ pq

0 commit comments

Comments
 (0)