-- | Examples how to use "Agda.Utils.Lens".

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
  }

-- | (View source:) This is how you implement a lens for a record field.
lensField1 :: Lens' a (Record a b)
lensField1 :: forall a b. Lens' a (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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ a
a -> Record a b
r { field1 :: a
field1 = a
a }

lensField2 :: Lens' b (Record a b)
lensField2 :: forall b a. Lens' b (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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ b
b -> Record a b
r { field2 :: b
field2 = b
b }