Leanses library

Lens implementation for Lean 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.

import Leanses

structure SubEx where
  c : String
  deriving Repr

-- `mklenses` automatically generates lenses for a structure.
mklenses SubEx
open SubEx.l

structure Example where
  s1 : String
  s2 : Int
  s3 : SubEx
  deriving Repr

mklenses Example
open Example.l

def v := Example.mk "a" 1 {c := "c"}

-- Structure update syntax built into Lean
/--
info: let __src := v;
{ s1 := "b", s2 := 5, s3 := __src.s3 } : Example
-/
#guard_msgs in
#check { v with s2 := 5, s1 := "b" }

/--
info: let __src := v;
{ s1 := "c", s2 := __src.s2,
  s3 :=
    let __src := __src.s3;
    { c := "deep" } } : Example
-/
#guard_msgs in
#check { v with s3.c := "deep", s1 := "c" }

-- Structure updates using lenses

/--
info: <{ v with s2 := 5, s1 := "b" }> : Example
-/
#guard_msgs in
#check <{ v with s2 := 5, s1 := "b" }>

/--
info: <{ v with s3∘∘c := "deep", s1 := "c" }> : Example
-/
#guard_msgs in
#check <{ v with s3∘∘c := "deep", s1 := "c" }>

set_option pp.hideLensUpdates true

/--
info: <{ v ... }> : Example
-/
#guard_msgs in
#check <{ v with s2 := 5, s1 := "b" }>

/--
info: <{ v ... }> : Example
-/
#guard_msgs in
#check <{ v with s3∘∘c := "deep", s1 := "c" }>