def Lean.Parser.«command_Grind_propagator___(_):=_» : Lean.ParserDescr

A user-defined propagator for the grind tactic.

Equations

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

def Lean.Parser.«command_Builtin_grind_propagator____:=_» : Lean.ParserDescr

A builtin propagator for the grind tactic.

Equations

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

def Lean.Parser.grindPropagatorBuiltinAttr : Lean.ParserDescr

Auxiliary attribute for builtin grind propagators.

Equations

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