Claude-skill-registry collimator

Guide for using Collimator, a profunctor optics library for Lean 4. Use when writing code with lenses, prisms, traversals, or when accessing/modifying nested data structures.

install

source · Clone the upstream repo

git clone https://github.com/majiayu000/claude-skill-registry

Claude Code · Install into ~/.claude/skills/

T=$(mktemp -d) && git clone --depth=1 https://github.com/majiayu000/claude-skill-registry "$T" && mkdir -p ~/.claude/skills && cp -r "$T/skills/data/collimator" ~/.claude/skills/majiayu000-claude-skill-registry-collimator && rm -rf "$T"

manifest: skills/data/collimator/SKILL.md

Collimator Optics Library

Overview

Collimator is a profunctor optics library for Lean 4. Optics provide composable, type-safe access patterns for nested data structures.

Imports

import Collimator.Prelude      -- Core optic types and operations
import Collimator.Operators    -- Haskell-style operators
import Collimator.Combinators  -- Advanced combinators
import Collimator.Instances    -- Instances for List, Option, String

open Collimator
open scoped Collimator.Operators  -- Enable operator syntax

Optic Types

Optic	Focus	Read	Write
`Iso' s a`	Exactly 1 (reversible)	Yes	Yes
`Lens' s a`	Exactly 1	Yes	Yes
`Prism' s a`	0 or 1 (sum types)	Maybe	Yes
`AffineTraversal' s a`	0 or 1	Maybe	Yes
`Traversal' s a`	0 or more	List	Yes

Operators

data ^. optic           -- View (Lens, Iso)
data ^? optic           -- Preview optional (Prism, AffineTraversal)
data ^.. optic          -- Collect all (Traversal)
data & optic %~ f       -- Modify with function
data & optic .~ value   -- Set value

Creating Optics

Lenses (struct fields)

structure Person where
  name : String
  age : Nat

-- Preferred: use fieldLens% macro
def nameLens : Lens' Person String := fieldLens% Person name

Prisms (sum type constructors)

inductive JsonValue
  | str : String → JsonValue
  | num : Int → JsonValue

-- Preferred: use ctorPrism% macro
def strPrism : Prism' JsonValue String := ctorPrism% JsonValue.str

-- For Option.some
def somePrism (α : Type) : Prism' (Option α) α := ctorPrism% Option.some

Composition

Optics compose with

∘

. Use

optic%

for type annotations:

-- Lens ∘ Prism = AffineTraversal
let emailAffine := optic%
  userProfileLens ∘ somePrism Profile ∘ emailLens
  : AffineTraversal' User String

user ^? emailAffine              -- Option String
user & emailAffine %~ toUpper    -- Modify if present

Common Patterns

Filtering

[-1, 2, -3, 4] & filteredList (· > 0) %~ (· * 2)  -- [-1, 4, -3, 8]

List operations

[1, 2, 3] ^? _head                    -- some 1
[1, 2, 3, 4] & taking 2 %~ (· * 10)   -- [10, 20, 3, 4]

Bifunctors

(3, 5) & both %~ (· * 2)  -- (6, 10)

Built-in Instances

List:
```
traversed
```
,
```
itraversed
```
,
```
atLens
```
,
```
ix
```
Option:
```
somePrism' α
```
,
```
traversed
```
String:
```
chars
```
(Iso),
```
traversed
```
Tuples:
```
_1
```
,
```
_2
```