Legacy tactic configuration elaboration

This module exists for reverse compatibility — users should import Lean.Elab.ConfigEval directly. It has been deprecated since 2026-05-14 and will be removed.

The new declare_config_elab and declare_command_config_elab commands are generally drop-in replacements for the legacy ones.

Migration notes:

• You may need to add a where except field1, field2, ... clause to omit things like function fields that do not have expression interpreters (e.g. Lean.Elab.Tactic.SolveByElim.elabConfig)
• You may choose to use derive_eval_expr_instance_using_meta_eval to derive a Meta.evalTerm'-based expression evaluator for one or more fields, or for the configuration structure itself to support the (config := ...) option, replicating the technique used in this module. Note that these instances are slow.
• If all else fails, until this module is removed there are the declare_config_elab_legacy and declare_command_config_elab_legacy commands.

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.

def Lean.Elab.Tactic.configElab : ParserDescr

declare_config_elab_legacy 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.

This command has been deprecated since 2026-05-14. Use declare_config_elab instead.

Equations

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

def Lean.Elab.Tactic.commandConfigElab : ParserDescr

declare_command_config_elab_legacy 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.

This command has been deprecated since 2026-05-14. Use declare_command_config_elab instead.

Equations

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