    -- | 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
      { field1 :: a
      , field2 :: b
      }

    -- | (View source:) This is how you implement a lens for a record field.
    lensField1 :: Lens' a (Record a b)
    lensField1 f r = f (field1 r) <&> \ a -> r { field1 = a }

    lensField2 :: Lens' b (Record a b)
    lensField2 f r = f (field2 r) <&> \ b -> r { field2 = b }