{-# OPTIONS_GHC -Wunused-imports #-}
module Agda.Utils.Lens.Examples where
import Agda.Utils.Functor
import Agda.Utils.Lens
data Record a b = Record
{ forall a b. Record a b -> a
field1 :: a
, forall a b. Record a b -> b
field2 :: b
}
lensField1 :: Lens' (Record a b) a
lensField1 :: forall a b (f :: * -> *).
Functor f =>
(a -> f a) -> Record a b -> f (Record a b)
lensField1 a -> f a
f Record a b
r = a -> f a
f (Record a b -> a
forall a b. Record a b -> a
field1 Record a b
r) f a -> (a -> Record a b) -> f (Record a b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ a
a -> Record a b
r { field1 = a }
lensField2 :: Lens' (Record a b) b
lensField2 :: forall a b (f :: * -> *).
Functor f =>
(b -> f b) -> Record a b -> f (Record a b)
lensField2 b -> f b
f Record a b
r = b -> f b
f (Record a b -> b
forall a b. Record a b -> b
field2 Record a b
r) f b -> (b -> Record a b) -> f (Record a b)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ b
b -> Record a b
r { field2 = b }