Lean4
/-- The `push` attribute is used to tag lemmas that "push" a constant into an expression.
For example:
```lean
@[push] theorem log_mul (hx : x ≠ 0) (hy : y ≠ 0) : log (x * y) = log x + log y
@[push] theorem log_abs : log |x| = log x
@[push] theorem not_imp (p q : Prop) : ¬(p → q) ↔ p ∧ ¬q
@[push] theorem not_iff (p q : Prop) : ¬(p ↔ q) ↔ (p ∧ ¬q) ∨ (¬p ∧ q)
@[push] theorem not_not (p : Prop) : ¬ ¬p ↔ p
@[push] theorem not_le : ¬a ≤ b ↔ b < a
```
Note that some `push` lemmas don't push the constant away from the head (`log_abs`) and
some `push` lemmas cancel the constant out (`not_not` and `not_le`).
For the other lemmas that are "genuine" `push` lemmas, a `pull` attribute is automatically added
in the reverse direction. To not add a `pull` tag, use `@[push only]`.
To tag the reverse direction of the lemma, use `@[push ←]`.
-/
@[attr_parser 1000]
public meta def pushAttr : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.Push.pushAttr 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "push" false✝)
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `orelse (ParserDescr.nodeWithAntiquot✝ " ←" `token.« ←» (ParserDescr.symbol✝ " ←"))
(ParserDescr.nodeWithAntiquot✝ " <-" `token.« <-» (ParserDescr.symbol✝ " <-")))))
(ParserDescr.unary✝ `optional ((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) " only" false✝)))
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.cat✝ `prio 0))))
