From c8dfbb51899ce3f02f23658329c1fa8acec34fe7 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Sat, 4 Mar 2023 23:56:35 -0500 Subject: [PATCH] Fix profunctor record declarations --- Data/Profunctor/Types.idr | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Data/Profunctor/Types.idr b/Data/Profunctor/Types.idr index d8c2572..585231a 100644 --- a/Data/Profunctor/Types.idr +++ b/Data/Profunctor/Types.idr @@ -44,7 +44,7 @@ Functor f => Profunctor (Kleislimorphism f) where -- Examples of profunctors public export -record Star (f : k -> Type) a (b : k) where +record Star {0 k : Type} (f : k -> Type) a (b : k) where constructor MkStar applyStar : a -> f b @@ -76,7 +76,7 @@ Functor f => Profunctor (Star f) where public export -record Costar (f : k -> Type) (a : k) b where +record Costar {0 k : Type} (f : k -> Type) (a : k) b where constructor MkCostar applyCostar : f a -> b @@ -101,7 +101,7 @@ Functor f => Profunctor (Costar f) where public export -record Tagged (a : k) b where +record Tagged {0 k : Type} (a : k) b where constructor Tag getTagged : b