lean-optics

lean-optics is a Lean 4 package that implements profunctor-style optics: Lens, Prism, Traversal, plus law-preserving composition.

Install and import

Add this dependency to your lakefile.toml:

[[require]]
name = "lean-optics"
git = "https://github.com/fraware/lean-optics.git"
rev = "main"

Stable API (no macros):

import Optics

Automation (macros, derive_lens, tactics):

import Optics.Automation

Minimal example (macro-free)

import Optics

structure Person where
  name : String
  age : Nat

def nameLens : LawfulLens Person String :=
  Lens.mkLawful
    (get := Person.name)
    (set := fun p n => { p with name := n })
    (by intro _ _; rfl) (by intro _; rfl) (by intro _ _ _; rfl)

def renamed : Person :=
  nameLens.over (fun n => n.toUpper) { name := "Alice", age := 30 }

See Optics.Examples.LawfulLens and Optics.Examples.MachineState for upstream extraction examples. The CSLib proposal lives at docs/upstream/CSLIB_LENS_PROPOSAL.md.

Build and verify

lake update
lake build
lake build tests testsAdvanced
lake exe test-runner
lake exe test-advanced
lake exe bench

Module layers

Layer	Import	Contents
Stable	Optics	Core, lawful lens, prism, traversal, compose
Automation	Optics.Automation	lens!, prism!, derive_lens, tactics
Experimental	Optics.Experimental	Container traversals, telemetry, verification

License

MIT. See LICENSE.