Applicative: do not export private module M

agda · Nov 10, 2023 · 30c253e · 30c253e
1 parent 3e96662
commit 30c253e
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Class/Applicative/Instances.agda b/Class/Applicative/Instances.agda
@@ -51,7 +51,7 @@ instance
   --   .pure x → 1 , pure x
   --   ._<*>_ (n , xs) (m , ys) → {! (n ⊔ m) , zipWith _$_ xs ys  -- (+ zipWith-⊔ lemma) !}
 
-  module M where
+  private module M where
     open import Reflection.TCM.Syntax public
     open import Reflection.TCM public