Documentation

Lean.Elab.Tactic.Grind.Config

source
def Lean.Elab.Tactic.Grind.setConfigField :
Grind.Config → Name → DataValue → TermElabM Grind.Config

Sets a field of the grind configuration object.

Equations
    Instances For
      source
      def Lean.Elab.Tactic.Grind.elabConfigItems (init : Grind.Config) (items : Array (TSyntax `Lean.Parser.Tactic.configItem)) :
      TermElabM Grind.Config
      Equations
        Instances For
          source
          def Lean.Elab.Tactic.Grind.withConfigItems {α : Type} (items : Array (TSyntax `Lean.Parser.Tactic.configItem)) (k : GrindTacticM α) :
          GrindTacticM α
          Equations
            Instances For