structure Lean.Elab.Tactic.ConfigItemView : Type

• ref : Syntax
• option : Ident
• value : Term
• bool : Bool

  Whether this was using +/-, to be able to give a better error message on type mismatch.

def Lean.Elab.Tactic.mkConfigItemViews (c : TSyntaxArray `Lean.Parser.Tactic.configItem) : Array ConfigItemView

Interprets the config as an array of option/value pairs.

def Lean.Elab.Tactic.elabConfig (recover : Bool) (structName : Name) (items : Array ConfigItemView) : TermElabM Expr

Elaborates a tactic configuration.

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

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