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.

Equations

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

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

Elaborates a tactic configuration.

Equations

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

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

Equations

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

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

Equations

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