From a7152cd5823080c35392982abdb4a3bfafe2f81d Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Sat, 4 Nov 2023 20:58:54 -0400 Subject: [PATCH] Combine fixity declarations Apparently this is something you can do? I wasn't aware of it, but it's very useful! --- src/Control/Lens/Getter.idr | 3 +-- src/Control/Lens/Indexed.idr | 4 +--- src/Control/Lens/Lens.idr | 17 +++++------------ src/Control/Lens/Setter.idr | 12 +++--------- 4 files changed, 10 insertions(+), 26 deletions(-) diff --git a/src/Control/Lens/Getter.idr b/src/Control/Lens/Getter.idr index 6b57f21..185f8db 100644 --- a/src/Control/Lens/Getter.idr +++ b/src/Control/Lens/Getter.idr @@ -85,8 +85,7 @@ iview : IndexedGetter i s a -> s -> (i, a) iview l = runForget $ l @{%search} @{Idxed} $ MkForget id -infixl 8 ^. -infixl 8 ^@. +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 c48214c..f031000 100644 --- a/src/Control/Lens/Indexed.idr +++ b/src/Control/Lens/Indexed.idr @@ -93,9 +93,7 @@ icompose @{MkIsIso _} f l l' @{ind} = l @{Idxed} . runIndexed . l' @{Idxed} . MkIndexed {p} . lmap (mapFst (uncurry f) . assocl) . indexed @{ind} -infixr 9 <.> -infixr 9 .> -infixr 9 <. +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 edd738d..c3a6cd2 100644 --- a/src/Control/Lens/Lens.idr +++ b/src/Control/Lens/Lens.idr @@ -139,20 +139,13 @@ fusing @{MkIsIso _} l = proextract . l . propure -- Operators ------------------------------------------------------------------------------ -infixr 4 %%~; infix 4 %%=; infix 4 %%@~; infix 4 %%@= +infixr 4 %%~, %%=, %%@~, %%@= -infixr 4 <%~; infixr 4 <%@~; infixr 4 <+~; infixr 4 <*~; infixr 4 <-~ -infixr 4 ~ +infixr 4 <%~, <%@~, <+~, <*~, <-~, ~ +infixr 4 <<%~, <<%@~, <<.~, <~ -infixr 4 <<%~; infixr 4 <<%@~; infixr 4 <<.~; infixr 4 <~ - -infix 4 <%=; infix 4 <%@=; infix 4 <+=; infix 4 <*=; infix 4 <-=; infix 4 = - -infix 4 <<%=; infix 4 <<%@=; infix 4 <<.=; infix 4 <= +infix 4 <%=, <%@=, <+=, <*=, <-=, = +infix 4 <<%=, <<%@=, <<.=, <= infixr 1 <<<~ diff --git a/src/Control/Lens/Setter.idr b/src/Control/Lens/Setter.idr index cd82eb5..a915afd 100644 --- a/src/Control/Lens/Setter.idr +++ b/src/Control/Lens/Setter.idr @@ -150,15 +150,9 @@ public export -- More operators ------------------------------------------------------------------------------ -infixr 4 ?~; infixr 4 <.~; infixr 4 ~ - -infix 4 %=; infix 4 %@=; infix 4 .=; infix 4 .@=; infix 4 ?=; infix 4 <.= -infix 4 = - -infix 1 <~ -infixr 1 <<~ +infixr 4 ?~, <.~, ~ +infix 4 %=, %@=, .=, .@=, ?=, <.=, = +infix 1 <~, <<~ ||| Set the focus of an optic to `Just` a value. public export