HepLean Documentation

Lean.Elab.Tactic.Config

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 :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Elab.Tactic.checkConfigElab :
    Lean.Linter.MissingDocs.SimpleHandler
    Equations
    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 :
      Lean.ParserDescr
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Lean.Elab.Tactic.checkCommandConfigElab :
        Lean.Linter.MissingDocs.SimpleHandler
        Equations
        Instances For