def Lean.Elab.mkConfigSetter (doc? : Option (TSyntax `Lean.Parser.Command.docComment)) (setterName struct : Ident) : Command.CommandElabM Unit

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.

def Lean.Elab.elabConfigGetter : ParserDescr

Equations

• One or more equations did not get rendered due to their size.