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

^.

person ^. personName

^?

val ^? _someVariant

.~

person & personAge .~ 30

%~

person & personAge %~ (· + 1)

&

x & lens .~ v

∘

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)