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.