From 60231f4a2bbc830be96da6ab83ef44560db618a1 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Sat, 29 Jun 2024 01:42:08 -0400 Subject: [PATCH] Add export declaration to fixities --- src/Control/Lens/Fold.idr | 8 +------- src/Control/Lens/Getter.idr | 2 +- src/Control/Lens/Indexed.idr | 2 +- src/Control/Lens/Lens.idr | 12 ++++++------ src/Control/Lens/Review.idr | 2 +- src/Control/Lens/Setter.idr | 14 ++++---------- src/Control/Zipper.idr | 2 +- src/Data/Maybe/Lens.idr | 2 +- 8 files changed, 16 insertions(+), 28 deletions(-) diff --git a/src/Control/Lens/Fold.idr b/src/Control/Lens/Fold.idr index 67ff90d..e98c9ac 100644 --- a/src/Control/Lens/Fold.idr +++ b/src/Control/Lens/Fold.idr @@ -287,7 +287,7 @@ public export preview : Fold s a -> s -> Maybe a preview = firstOf -infixl 8 ^? +export infixl 8 ^?, ^@?, ^., ^@. ||| Access the first focus value of an optic, returning `Nothing` if there are ||| no focuses. @@ -306,8 +306,6 @@ public export ipreview : IndexedFold i s a -> s -> Maybe (i, a) ipreview = ifirstOf -infixl 8 ^@? - ||| Access the first focus value and index of an indexed optic, returning Nothing ||| if there are no focuses. ||| @@ -338,8 +336,6 @@ public export toListOf : Fold s a -> s -> List a toListOf l = foldrOf l (::) [] -infixl 8 ^.. - ||| Return a list of all focuses of a fold. ||| ||| This is the operator form of `toListOf`. @@ -353,8 +349,6 @@ public export itoListOf : IndexedFold i s a -> s -> List (i, a) itoListOf l = ifoldrOf l ((::) .: (,)) [] -infixl 8 ^@.. - ||| Return a list of all focuses and indices of an indexed fold. ||| ||| This is the operator form of `itoListOf`. diff --git a/src/Control/Lens/Getter.idr b/src/Control/Lens/Getter.idr index 185f8db..bdaaf04 100644 --- a/src/Control/Lens/Getter.idr +++ b/src/Control/Lens/Getter.idr @@ -85,7 +85,7 @@ iview : IndexedGetter i s a -> s -> (i, a) iview l = runForget $ l @{%search} @{Idxed} $ MkForget id -infixl 8 ^., ^@. +export infixl 8 ^., ^@. ||| Access the focus value of an optic, particularly a `Getter`. ||| diff --git a/src/Control/Lens/Indexed.idr b/src/Control/Lens/Indexed.idr index f031000..a558a63 100644 --- a/src/Control/Lens/Indexed.idr +++ b/src/Control/Lens/Indexed.idr @@ -93,7 +93,7 @@ icompose @{MkIsIso _} f l l' @{ind} = l @{Idxed} . runIndexed . l' @{Idxed} . MkIndexed {p} . lmap (mapFst (uncurry f) . assocl) . indexed @{ind} -infixr 9 <.>, .>, <. +export infixr 9 <.>, .>, <. ||| Compose two indexed optics, returning an optic indexed by a pair of indices. ||| diff --git a/src/Control/Lens/Lens.idr b/src/Control/Lens/Lens.idr index c3a6cd2..d702d3b 100644 --- a/src/Control/Lens/Lens.idr +++ b/src/Control/Lens/Lens.idr @@ -139,15 +139,15 @@ fusing @{MkIsIso _} l = proextract . l . propure -- Operators ------------------------------------------------------------------------------ -infixr 4 %%~, %%=, %%@~, %%@= +export infixr 4 %%~, %%=, %%@~, %%@= -infixr 4 <%~, <%@~, <+~, <*~, <-~, ~ -infixr 4 <<%~, <<%@~, <<.~, <~ +export infixr 4 <%~, <%@~, <+~, <*~, <-~, ~ +export infixr 4 <<%~, <<%@~, <<.~, <~ -infix 4 <%=, <%@=, <+=, <*=, <-=, = -infix 4 <<%=, <<%@=, <<.=, <= +export infix 4 <%=, <%@=, <+=, <*=, <-=, = +export infix 4 <<%=, <<%@=, <<.=, <= -infixr 1 <<<~ +export infixr 1 <<<~ public export diff --git a/src/Control/Lens/Review.idr b/src/Control/Lens/Review.idr index 0f03544..c49e9c0 100644 --- a/src/Control/Lens/Review.idr +++ b/src/Control/Lens/Review.idr @@ -66,7 +66,7 @@ public export review : Review s a -> a -> s review l = reviews l id -infixr 8 ^$ +export infixr 8 ^$ ||| Turn an optic around to inject a focus value into the larger data structure. ||| This function takes a `Review`, which can also be a `Prism` or `Iso`. diff --git a/src/Control/Lens/Setter.idr b/src/Control/Lens/Setter.idr index a915afd..1cc2a54 100644 --- a/src/Control/Lens/Setter.idr +++ b/src/Control/Lens/Setter.idr @@ -91,7 +91,7 @@ public export over : Setter s t a b -> (a -> b) -> s -> t over l = l @{MkIsSetter Function} -infixr 4 %~ +export infixr 4 %~, %@~, .~, .@~ ||| Modify the focus or focuses of an optic. ||| @@ -106,8 +106,6 @@ public export iover : IndexedSetter i s t a b -> (i -> a -> b) -> s -> t iover l = l @{MkIsSetter Function} @{Idxed} . uncurry -infixr 4 %@~ - ||| Modify the focus or focuses of an indexed optic, having access to the index. ||| ||| This is the operator form of `iover`. @@ -121,8 +119,6 @@ public export set : Setter s t a b -> b -> s -> t set l = over l . const -infixr 4 .~ - ||| Set the focus or focuses of an optic to a constant value. ||| ||| This is the operator form of `set`. @@ -136,8 +132,6 @@ public export iset : IndexedSetter i s t a b -> (i -> b) -> s -> t iset l = iover l . (const .) -infix 4 .@~ - ||| Set the focus or focuses of an indexed optic, having access to the index. ||| ||| This is the operator form of `iset`. @@ -150,9 +144,9 @@ public export -- More operators ------------------------------------------------------------------------------ -infixr 4 ?~, <.~, ~ -infix 4 %=, %@=, .=, .@=, ?=, <.=, = -infix 1 <~, <<~ +export infixr 4 ?~, <.~, ~ +export infix 4 %=, %@=, .=, .@=, ?=, <.=, = +export infix 1 <~, <<~ ||| Set the focus of an optic to `Just` a value. public export diff --git a/src/Control/Zipper.idr b/src/Control/Zipper.idr index d6c450a..d293fb3 100644 --- a/src/Control/Zipper.idr +++ b/src/Control/Zipper.idr @@ -27,7 +27,7 @@ fromPointer k x (l, r) = l <>> (k,x) :: r ------------------------------------------------------------------------------ -infix 9 @> +export infix 9 @> ||| A simple type that represents a layer of the zipper as it moves downwards. ||| diff --git a/src/Data/Maybe/Lens.idr b/src/Data/Maybe/Lens.idr index 9f0eaad..67a754f 100644 --- a/src/Data/Maybe/Lens.idr +++ b/src/Data/Maybe/Lens.idr @@ -19,7 +19,7 @@ Just_ = prism Just $ \case Nothing => Left Nothing Just x => Right x -infixl 9 .? +export infixl 9 .? ||| The composition `l .? l'` is equivalent to `l . Just_ . l'`. ||| Useful for optics whose focus type is a `Maybe`, such as `at`.