From cf38f4a07e78e1e409cc6cfdb44e1e65e53f41c6 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Mon, 6 Mar 2023 10:52:28 -0500 Subject: [PATCH] Use forall instead of implicit argument notation --- Data/Profunctor/Strong.idr | 2 +- Data/Profunctor/Types.idr | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Data/Profunctor/Strong.idr b/Data/Profunctor/Strong.idr index da0aba5..3e5d4a7 100644 --- a/Data/Profunctor/Strong.idr +++ b/Data/Profunctor/Strong.idr @@ -48,7 +48,7 @@ uncurry' = rmap (uncurry id) . first public export record GenTambara (ten, p : Type -> Type -> Type) a b where constructor MkTambara - getTambara : {0 c : Type} -> p (a `ten` c) (b `ten` c) + getTambara : forall c. p (a `ten` c) (b `ten` c) export Bifunctor ten => Profunctor p => Profunctor (GenTambara ten p) where diff --git a/Data/Profunctor/Types.idr b/Data/Profunctor/Types.idr index 60ae243..9bc72b4 100644 --- a/Data/Profunctor/Types.idr +++ b/Data/Profunctor/Types.idr @@ -22,7 +22,7 @@ interface Profunctor p where infix 0 :-> public export 0 (:->) : (p, q : k -> k' -> Type) -> Type -p :-> q = {0 a, b : _} -> p a b -> q a b +p :-> q = forall a, b. p a b -> q a b -- Instances for existing types