@[reducible, inline]

abbrev Lean.Elab.Tactic.Grind.SymDSimprocElab : Type

Elaboration function for sym_dsimproc syntax.

Equations

• Lean.Elab.Tactic.Grind.SymDSimprocElab = (Lean.Syntax → Lean.Elab.Tactic.Grind.GrindTacticM Lean.Meta.Sym.DSimp.DSimproc)

opaque Lean.Elab.Tactic.Grind.symDSimprocElabAttribute : KeyedDeclsAttribute SymDSimprocElab

def Lean.Elab.Tactic.Grind.elabSymDSimproc (stx : Syntax) : GrindTacticM Meta.Sym.DSimp.DSimproc

Elaborate a sym_dsimproc syntax node into a DSimproc.

Equations

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