Lean4
/-- `eta_struct at loc` transforms structure constructor applications such as `S.mk x.1 ... x.n`
(pretty printed as, for example, `{a := x.a, b := x.b, ...}`) into `x`.
This also exists as a `conv`-mode tactic.
The transformation is known as eta reduction for structures, and it yields definitionally
equal expressions.
For example, given `x : α × β`, then `(x.1, x.2)` becomes `x` after this transformation.
-/
@[tactic_parser 1000]
public meta def etaStructStx : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.etaStructStx 1022
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "eta_struct" false✝)
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) Lean.Parser.Tactic.location)))
