Lean4
/-- `eta_expand at loc` eta expands all sub-expressions at the given location.
It also beta reduces any applications of eta expanded terms, so it puts it
into an eta-expanded "normal form."
This also exists as a `conv`-mode tactic.
For example, if `f` takes two arguments, then `f` becomes `fun x y => f x y`
and `f x` becomes `fun y => f x y`.
This can be useful to turn, for example, a raw `HAdd.hAdd` into `fun x y => x + y`.
-/
@[tactic_parser 1000]
public meta def etaExpandStx : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.etaExpandStx 1022
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "eta_expand" false✝)
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) Lean.Parser.Tactic.location)))
