Collimator Optics Quick Reference

Setup

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

Generate Lenses (Preferred)

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

Operators

| Op | Name | Example | |----|------|---------| | ^. | view | person ^. personName | | ^? | preview | val ^? _someVariant | | .~ | set | person & personAge .~ 30 | | %~ | over | person & personAge %~ (· + 1) | | & | pipe | x & lens .~ v | | ∘ | compose | outer ∘ inner |

Prisms for Sum Types

def _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:

import 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

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