declare_config_elab elabName TypeName declares a function elabName : Syntax → TacticM TypeName that elaborates a tactic configuration. The tactic configuration can be from Lean.Parser.Tactic.optConfig or Lean.Parser.Tactic.config, and these can also be wrapped in null nodes (for example, from (config)?).

The elaborator responds to the current recovery state.

For defining elaborators for commands, use declare_command_config_elab.

def Lean.Elab.Tactic.configElab : ParserDescr

def Lean.Elab.Tactic.checkConfigElab : Linter.MissingDocs.SimpleHandler

declare_command_config_elab elabName TypeName declares a function elabName : Syntax → CommandElabM TypeName that elaborates a command configuration. The configuration can be from Lean.Parser.Tactic.optConfig or Lean.Parser.Tactic.config, and these can also be wrapped in null nodes (for example, from (config)?).

The elaborator has error recovery enabled.

def Lean.Elab.Tactic.commandConfigElab : ParserDescr

def Lean.Elab.Tactic.checkCommandConfigElab : Linter.MissingDocs.SimpleHandler