Documentation

Lean.Elab.Tactic.Grind.DSimprocDSL

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

Elaboration function for sym_dsimproc syntax.

Instances For
    source
    opaque Lean.Elab.Tactic.Grind.symDSimprocElabAttribute :
    KeyedDeclsAttribute SymDSimprocElab
    source
    def Lean.Elab.Tactic.Grind.elabSymDSimproc (stx : Syntax) :
    GrindTacticM Meta.Sym.DSimp.DSimproc

    Elaborate a sym_dsimproc syntax node into a DSimproc.

    Instances For