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" }>