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.

Instances For
    source
    def Lean.Elab.Tactic.Grind.elabConfigItems (init : Grind.Config) (items : Array (TSyntax `Lean.Parser.Tactic.configItem)) :
    TermElabM Grind.Config
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.Elab.Tactic.Grind.withConfigItems {α : Type} (items : Array (TSyntax `Lean.Parser.Tactic.configItem)) (k : GrindTacticM α) :
      GrindTacticM α
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For