fixes #2467 (#2468)

agda · Aug 30, 2024 · cc69ea0 · cc69ea0
1 parent 355ac25
commit cc69ea0
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Data/List/Relation/Unary/All.agda b/src/Data/List/Relation/Unary/All.agda
@@ -115,7 +115,7 @@ zip = zipWith id
 unzip : All (P ∩ Q) ⊆ All P ∩ All Q
 unzip = unzipWith id
 
-module _(S : Setoid a ℓ) {P : Pred (Setoid.Carrier S) p} where
+module _ (S : Setoid a ℓ) {P : Pred (Setoid.Carrier S) p} where
   open Setoid S renaming (refl to ≈-refl)
   open SetoidMembership S