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