Documentation

Lean.Elab.Tactic.Grind.SimprocDSL

source
@[reducible, inline]
abbrev Lean.Elab.Tactic.Grind.SymSimprocElab :
Type

Elaboration function for sym_simproc syntax.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Lean.Elab.Tactic.Grind.SymDischargerElab :
    Type

    Elaboration function for sym_discharger syntax.

    Equations
    Instances For
      source
      opaque Lean.Elab.Tactic.Grind.symSimprocElabAttribute :
      KeyedDeclsAttribute SymSimprocElab
      source
      opaque Lean.Elab.Tactic.Grind.symDischargerElabAttribute :
      KeyedDeclsAttribute SymDischargerElab
      source
      def Lean.Elab.Tactic.Grind.elabSymSimproc (stx : Syntax) :
      GrindTacticM Meta.Sym.Simp.Simproc

      Elaborate a sym_simproc syntax node into a Simproc.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Lean.Elab.Tactic.Grind.elabSymDischarger (stx : Syntax) :
        GrindTacticM Meta.Sym.Simp.Discharger

        Elaborate a sym_discharger syntax node into a Discharger.

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