LeansesΒΆ

Lens implementation for Lean 4 with custom update notation and pretty-printing. Updates can also be hidden using pp.hideLensUpdates. Using lenses provides a more flexible record update syntax that can be manipulated to provide better pretty-printing of such updates.