    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | 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' (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 }