Lean4
/-- `apply (config := cfg) e` is like `apply e` but allows you to provide a configuration
`cfg : ApplyConfig` to pass to the underlying `apply` operation.
-/
@[tactic_parser 1000]
public meta def applyWith : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.applyWith 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "apply" false✝) (ParserDescr.symbol✝ " ("))
((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) "config" false✝))
(ParserDescr.symbol✝ " := "))
(ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ ") "))
(ParserDescr.cat✝ `term 0))
