toki/idris2-lens
1
0
Fork 0
Code Issues Pull requests Activity

Combine fixity declarations

Browse source 
Apparently this is something you can do? I wasn't aware of it,
but it's very useful!
This commit is contained in:
Kiana Sheibani 2023-11-04 20:58:54 -04:00
parent 1e6309237b
commit a7152cd582
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
4 changed files with 10 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Control/Lens/Getter.idr
View file

@ -85,8 +85,7 @@ iview : IndexedGetter i s a -> s -> (i, a)
iview l = runForget $ l @{%search} @{Idxed} $ MkForget id iview l = runForget $ l @{%search} @{Idxed} $ MkForget id
infixl 8 ^. infixl 8 ^., ^@.
infixl 8 ^@.
||| Access the focus value of an optic, particularly a `Getter`. ||| Access the focus value of an optic, particularly a `Getter`.
||| |||

4
src/Control/Lens/Indexed.idr
View file

@ -93,9 +93,7 @@ icompose @{MkIsIso _} f l l' @{ind} =
l @{Idxed} . runIndexed . l' @{Idxed} . MkIndexed {p} l @{Idxed} . runIndexed . l' @{Idxed} . MkIndexed {p}
. lmap (mapFst (uncurry f) . assocl) . indexed @{ind} . 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. ||| Compose two indexed optics, returning an optic indexed by a pair of indices.
||| |||

17
src/Control/Lens/Lens.idr
View file

@ -139,20 +139,13 @@ fusing @{MkIsIso _} l = proextract . l . propure
-- Operators -- 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 <<%~; infixr 4 <<%@~; infixr 4 <<.~; infixr 4 <<?~; infixr 4 <<+~ infix 4 <%=, <%@=, <+=, <*=, <-=, </=, <||=, <&&=, <<+>=
infixr 4 <<*~; infixr 4 <<-~; infixr 4 <</~; infixr 4 <<||~; infixr 4 <<&&~ infix 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 <<.=; infix 4 <<?=; infix 4 <<+=; infix 4 <<*=
infix 4 <<-=; infix 4 <</=; infix 4 <<||=; infix 4 <<&&=; infix 4 <<<+>=
infixr 1 <<<~ infixr 1 <<<~

12
src/Control/Lens/Setter.idr
View file

@ -150,15 +150,9 @@ public export
-- More operators -- More operators
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
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 1 <~, <<~
infix 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 4 <+>=
infix 1 <~
infixr 1 <<~
||| Set the focus of an optic to `Just` a value. ||| Set the focus of an optic to `Just` a value.
public export public export