Agent skill

collimator-optics

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

View SKILL.md on GitHub Repository
Stars 163
Forks 31

Install this agent skill to your Project

npx add-skill https://github.com/majiayu000/claude-skill-registry/tree/main/skills/data/collimator-optics

SKILL.md

Collimator Optics Quick Reference

Setup

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

Generate Lenses (Preferred)

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

lean
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:

lean
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

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

Didn't find tool you were looking for?

Be as detailed as possible for better results