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

Instances For

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

Instances For

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

Instances For

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

source
def Lean.Elab.Tactic.configElab :
ParserDescr
Equations

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

Instances For

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

source
def Lean.Elab.Tactic.commandConfigElab :
ParserDescr
Equations

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

Instances For