---

name: collimator-optics description: Use profunctor optics from the Collimator library for Lean 4. Use when working with lenses, prisms, traversals, or nested data access.

Collimator Optics Quick Reference

Setup

Copyimport Collimator
import Collimator.Derive.Lenses
open Collimator.Derive
open scoped Collimator.Operators

Generate Lenses (Preferred)

Copy-- In separate Optics.lean file (to avoid circular imports)
makeLenses Person      -- Generates: personName, personAge, etc.
makeLenses Address     -- Generates: addressCity, addressZip, etc.

Operators

Prisms for Sum Types

Copydef _left : Prism' (Either A B) A := ctorPrism% Either.left
def _right : Prism' (Either A B) B := ctorPrism% Either.right

-- Usage
either ^? _left          -- Option A
either & _left %~ f      -- modify if Left

Affine Traversals (0-or-1 Focus)

For HashMap/collection access where a key may or may not exist:

Copyimport Collimator.Indexed
import Collimator.Instances.Option

-- Compose: field lens → index lens → some prism
def itemAt (k : Key) : AffineTraversal' Container Item :=
  containerItems ∘ Collimator.Indexed.atLens k ∘ Collimator.Instances.Option.somePrism' Item

-- Usage
container ^? itemAt key           -- Option Item
(container ^? itemAt key).isSome  -- exists check

Common Patterns

Copy-- Nested access
employee ^. (employeeAddress ∘ addressCity)

-- Chained updates
config
  & configHost .~ "localhost"
  & configPort .~ 8080

-- Conditional via prism
if (val ^? _error).isSome then handleError else continue

File Organization

To avoid circular imports:

1. Put structures in Types.lean
2. Put makeLenses calls in Optics.lean (imports Types)
3. Put methods in other files (import Optics)