Zulip Chat Archive
Stream: lean4
Topic: deriving setter functions
Jakob von Raumer (Nov 12 2025 at 22:22):
Does anyone have a deriver for setter functions for structures? (Implemented by {s with ...})
Jovan Gerbscheid (Nov 12 2025 at 23:07):
You might find this interesting: #lean4 > Lens-like notation @ 💬
Last updated: Dec 20 2025 at 21:32 UTC