Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Utils.Lens.Examples

Description

Examples how to use Agda.Utils.Lens.

Synopsis

- data Record a b = Record {
  - field1 :: a
  - field2 :: b
  }
- lensField1 :: forall a b f. Functor f => (a -> f a) -> Record a b -> f (Record a b)
- lensField2 :: forall a b f. Functor f => (b -> f b) -> Record a b -> f (Record a b)

# Documentation

data Record a b Source #

Constructors

Record |

Fields

- field1 :: a
- field2 :: b

lensField1 :: forall a b f. Functor f => (a -> f a) -> Record a b -> f (Record a b) Source #

(View source:) This is how you implement a lens for a record field.

lensField2 :: forall a b f. Functor f => (b -> f b) -> Record a b -> f (Record a b) Source #