def
Lean.Elab.mkConfigSetter
(doc? : Option (TSyntax `Lean.Parser.Command.docComment))
(setterName struct : Ident)
:
Generates a function setterName for updating the Bool and Nat fields
of the structure struct.
This is a very simple implementation. There is no support for subobjects.